Theorem ralinexa

Description: A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005)

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

Proof

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