Theorem nrexralim

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

	Ref	Expression
Assertion	nrexralim	|- ( -. E. x e. A A. y e. B ( ph -> ps ) <-> A. x e. A E. y e. B ( ph /\ -. ps ) )

Proof

Step	Hyp	Ref	Expression
1		rexanali	|- ( E. y e. B ( ph /\ -. ps ) <-> -. A. y e. B ( ph -> ps ) )
2	1	ralbii	|- ( A. x e. A E. y e. B ( ph /\ -. ps ) <-> A. x e. A -. A. y e. B ( ph -> ps ) )
3		ralnex	|- ( A. x e. A -. A. y e. B ( ph -> ps ) <-> -. E. x e. A A. y e. B ( ph -> ps ) )
4	2 3	bitr2i	|- ( -. E. x e. A A. y e. B ( ph -> ps ) <-> A. x e. A E. y e. B ( ph /\ -. ps ) )