Metamath Proof Explorer


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 ) )