Description: Double restricted existential quantification. (Contributed by NM, 11-Nov-1995) Reduce dependencies on axioms. (Revised by Wolf Lammen, 10-Jan-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | r2ex | |- ( E. x e. A E. y e. B ph <-> E. x E. y ( ( x e. A /\ y e. B ) /\ ph ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r2al | |- ( A. x e. A A. y e. B -. ph <-> A. x A. y ( ( x e. A /\ y e. B ) -> -. ph ) ) |
|
2 | 1 | r2exlem | |- ( E. x e. A E. y e. B ph <-> E. x E. y ( ( x e. A /\ y e. B ) /\ ph ) ) |