Theorem exanali

Description: A transformation of quantifiers and logical connectives. (Contributed by NM, 25-Mar-1996) (Proof shortened by Wolf Lammen, 4-Sep-2014)

	Ref	Expression
Assertion	exanali	$$⊢\exists x\left(\phi \wedge \neg \psi \right)\leftrightarrow \neg \forall x\left(\phi \to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		annim	$$⊢\left(\phi \wedge \neg \psi \right)\leftrightarrow \neg \left(\phi \to \psi \right)$$
2	1	exbii	$$⊢\exists x\left(\phi \wedge \neg \psi \right)\leftrightarrow \exists x\neg \left(\phi \to \psi \right)$$
3		exnal	$$⊢\exists x\neg \left(\phi \to \psi \right)\leftrightarrow \neg \forall x\left(\phi \to \psi \right)$$
4	2 3	bitri	$$⊢\exists x\left(\phi \wedge \neg \psi \right)\leftrightarrow \neg \forall x\left(\phi \to \psi \right)$$