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