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

Metamath Proof Explorer

Theorem 2reu5lem1

Description: Lemma for 2reu5 . Note that E! x e. A E! y e. B ph does not mean "there is exactly one x in A and exactly one y in B such that ph holds"; see comment for 2eu5 . (Contributed by Alexander van der Vekens, 17-Jun-2017)

Ref Expression
Assertion 2reu5lem1 
|- ( 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 df-reu 
 |-  ( E! y e. B ph <-> E! y ( y e. B /\ ph ) )
2 1 reubii 
 |-  ( E! x e. A E! y e. B ph <-> E! x e. A E! y ( y e. B /\ ph ) )
3 df-reu 
 |-  ( E! x e. A E! y ( y e. B /\ ph ) <-> E! x ( x e. A /\ E! y ( y e. B /\ ph ) ) )
4 euanv 
 |-  ( E! y ( x e. A /\ ( y e. B /\ ph ) ) <-> ( x e. A /\ E! y ( y e. B /\ ph ) ) )
5 4 bicomi 
 |-  ( ( x e. A /\ E! y ( y e. B /\ ph ) ) <-> E! y ( x e. A /\ ( y e. B /\ ph ) ) )
6 3anass 
 |-  ( ( x e. A /\ y e. B /\ ph ) <-> ( x e. A /\ ( y e. B /\ ph ) ) )
7 6 bicomi 
 |-  ( ( x e. A /\ ( y e. B /\ ph ) ) <-> ( x e. A /\ y e. B /\ ph ) )
8 7 eubii 
 |-  ( E! y ( x e. A /\ ( y e. B /\ ph ) ) <-> E! y ( x e. A /\ y e. B /\ ph ) )
9 5 8 bitri 
 |-  ( ( x e. A /\ E! y ( y e. B /\ ph ) ) <-> E! y ( x e. A /\ y e. B /\ ph ) )
10 9 eubii 
 |-  ( E! x ( x e. A /\ E! y ( y e. B /\ ph ) ) <-> E! x E! y ( x e. A /\ y e. B /\ ph ) )
11 3 10 bitri 
 |-  ( E! x e. A E! y ( y e. B /\ ph ) <-> E! x E! y ( x e. A /\ y e. B /\ ph ) )
12 2 11 bitri 
 |-  ( E! x e. A E! y e. B ph <-> E! x E! y ( x e. A /\ y e. B /\ ph ) )