∀x(P(x)⇒Q)⇔(∃xP(x)⇒Q)

$ \forallの束縛変数が結果に影響しないとき、$ \existに変換できるやつ

証明

量化子の範囲を限定するver.も成立する

$ \because\forall x\in A:(P'(x)\implies Q)

$ \iff\forall x:(x\in A\implies(P'(x)\implies Q))

$ \iff\forall x:(x\in A\land P'(x)\implies Q)

となるので、$ x\in A\land P'(x)を新たに$ P(x)とおけば∀x(P(x)⇒Q)⇔(∃xP(x)⇒Q)を適用できる