Theorem rexanali

Description: A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005) (Proof shortened by Wolf Lammen, 27-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		dfrex2	$$⊢\exists x\in A\left(\phi \wedge \neg \psi \right)\leftrightarrow \neg \forall x\in A\neg \left(\phi \wedge \neg \psi \right)$$
2		iman	$$⊢\left(\phi \to \psi \right)\leftrightarrow \neg \left(\phi \wedge \neg \psi \right)$$
3	2	ralbii	$$⊢\forall x\in A\left(\phi \to \psi \right)\leftrightarrow \forall x\in A\neg \left(\phi \wedge \neg \psi \right)$$
4	1 3	xchbinxr	$$⊢\exists x\in A\left(\phi \wedge \neg \psi \right)\leftrightarrow \neg \forall x\in A\left(\phi \to \psi \right)$$