This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem r2exlem

Description: Lemma factoring out common proof steps in r2exf an r2ex . Introduced to reduce dependencies on axioms. (Contributed by Wolf Lammen, 10-Jan-2020)

Ref Expression
Hypothesis r2exlem.1 
|- ( A. x e. A A. y e. B -. ph <-> A. x A. y ( ( x e. A /\ y e. B ) -> -. ph ) )
Assertion r2exlem 
|- ( E. x e. A E. y e. B ph <-> E. x E. y ( ( x e. A /\ y e. B ) /\ ph ) )

Proof

Step Hyp Ref Expression
1 r2exlem.1 
 |-  ( A. x e. A A. y e. B -. ph <-> A. x A. y ( ( x e. A /\ y e. B ) -> -. ph ) )
2 exnal 
 |-  ( E. x -. A. y ( ( x e. A /\ y e. B ) -> -. ph ) <-> -. A. x A. y ( ( x e. A /\ y e. B ) -> -. ph ) )
3 2 1 xchbinxr 
 |-  ( E. x -. A. y ( ( x e. A /\ y e. B ) -> -. ph ) <-> -. A. x e. A A. y e. B -. ph )
4 exnalimn 
 |-  ( E. y ( ( x e. A /\ y e. B ) /\ ph ) <-> -. A. y ( ( x e. A /\ y e. B ) -> -. ph ) )
5 4 exbii 
 |-  ( E. x E. y ( ( x e. A /\ y e. B ) /\ ph ) <-> E. x -. A. y ( ( x e. A /\ y e. B ) -> -. ph ) )
6 ralnex2 
 |-  ( A. x e. A A. y e. B -. ph <-> -. E. x e. A E. y e. B ph )
7 6 con2bii 
 |-  ( E. x e. A E. y e. B ph <-> -. A. x e. A A. y e. B -. ph )
8 3 5 7 3bitr4ri 
 |-  ( E. x e. A E. y e. B ph <-> E. x E. y ( ( x e. A /\ y e. B ) /\ ph ) )