Theorem nrexralim

Description: Negation of a complex predicate calculus formula. (Contributed by FL, 31-Jul-2009)

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

Proof

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