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

Metamath Proof Explorer

Theorem 2reuswap2

Description: A condition allowing swap of uniqueness and existential quantifiers. (Contributed by Thierry Arnoux, 7-Apr-2017)

Ref Expression
Assertion 2reuswap2 
|- ( A. x e. A E* y ( y e. B /\ ph ) -> ( E! x e. A E. y e. B ph -> E! y e. B E. x e. A ph ) )

Proof

Step Hyp Ref Expression
1 df-ral 
 |-  ( A. x e. A E* y ( y e. B /\ ph ) <-> A. x ( x e. A -> E* y ( y e. B /\ ph ) ) )
2 moanimv 
 |-  ( E* y ( x e. A /\ ( y e. B /\ ph ) ) <-> ( x e. A -> E* y ( y e. B /\ ph ) ) )
3 2 albii 
 |-  ( A. x E* y ( x e. A /\ ( y e. B /\ ph ) ) <-> A. x ( x e. A -> E* y ( y e. B /\ ph ) ) )
4 1 3 bitr4i 
 |-  ( A. x e. A E* y ( y e. B /\ ph ) <-> A. x E* y ( x e. A /\ ( y e. B /\ ph ) ) )
5 2euswapv 
 |-  ( A. x E* y ( x e. A /\ ( y e. B /\ ph ) ) -> ( E! x E. y ( x e. A /\ ( y e. B /\ ph ) ) -> E! y E. x ( x e. A /\ ( y e. B /\ ph ) ) ) )
6 df-reu 
 |-  ( E! x e. A E. y e. B ph <-> E! x ( x e. A /\ E. y e. B ph ) )
7 r19.42v 
 |-  ( E. y e. B ( x e. A /\ ph ) <-> ( x e. A /\ E. y e. B ph ) )
8 df-rex 
 |-  ( E. y e. B ( x e. A /\ ph ) <-> E. y ( y e. B /\ ( x e. A /\ ph ) ) )
9 7 8 bitr3i 
 |-  ( ( x e. A /\ E. y e. B ph ) <-> E. y ( y e. B /\ ( x e. A /\ ph ) ) )
10 an12 
 |-  ( ( y e. B /\ ( x e. A /\ ph ) ) <-> ( x e. A /\ ( y e. B /\ ph ) ) )
11 10 exbii 
 |-  ( E. y ( y e. B /\ ( x e. A /\ ph ) ) <-> E. y ( x e. A /\ ( y e. B /\ ph ) ) )
12 9 11 bitri 
 |-  ( ( x e. A /\ E. y e. B ph ) <-> E. y ( x e. A /\ ( y e. B /\ ph ) ) )
13 12 eubii 
 |-  ( E! x ( x e. A /\ E. y e. B ph ) <-> E! x E. y ( x e. A /\ ( y e. B /\ ph ) ) )
14 6 13 bitri 
 |-  ( E! x e. A E. y e. B ph <-> E! x E. y ( x e. A /\ ( y e. B /\ ph ) ) )
15 df-reu 
 |-  ( E! y e. B E. x e. A ph <-> E! y ( y e. B /\ E. x e. A ph ) )
16 r19.42v 
 |-  ( E. x e. A ( y e. B /\ ph ) <-> ( y e. B /\ E. x e. A ph ) )
17 df-rex 
 |-  ( E. x e. A ( y e. B /\ ph ) <-> E. x ( x e. A /\ ( y e. B /\ ph ) ) )
18 16 17 bitr3i 
 |-  ( ( y e. B /\ E. x e. A ph ) <-> E. x ( x e. A /\ ( y e. B /\ ph ) ) )
19 18 eubii 
 |-  ( E! y ( y e. B /\ E. x e. A ph ) <-> E! y E. x ( x e. A /\ ( y e. B /\ ph ) ) )
20 15 19 bitri 
 |-  ( E! y e. B E. x e. A ph <-> E! y E. x ( x e. A /\ ( y e. B /\ ph ) ) )
21 5 14 20 3imtr4g 
 |-  ( A. x E* y ( x e. A /\ ( y e. B /\ ph ) ) -> ( E! x e. A E. y e. B ph -> E! y e. B E. x e. A ph ) )
22 4 21 sylbi 
 |-  ( A. x e. A E* y ( y e. B /\ ph ) -> ( E! x e. A E. y e. B ph -> E! y e. B E. x e. A ph ) )