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

Metamath Proof Explorer

Theorem 2rmoswap

Description: A condition allowing to swap restricted "at most one" and restricted existential quantifiers, analogous to 2moswap . (Contributed by Alexander van der Vekens, 25-Jun-2017)

Ref Expression
Assertion 2rmoswap 
|- ( A. x e. A E* 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-rmo 
 |-  ( E* y e. B ph <-> E* y ( y e. B /\ ph ) )
2 1 ralbii 
 |-  ( A. x e. A E* y e. B ph <-> A. x e. A E* y ( y e. B /\ ph ) )
3 df-ral 
 |-  ( A. x e. A E* y ( y e. B /\ ph ) <-> A. x ( x e. A -> E* y ( y e. B /\ ph ) ) )
4 moanimv 
 |-  ( E* y ( x e. A /\ ( y e. B /\ ph ) ) <-> ( x e. A -> E* y ( y e. B /\ ph ) ) )
5 4 albii 
 |-  ( A. x E* y ( x e. A /\ ( y e. B /\ ph ) ) <-> A. x ( x e. A -> E* y ( y e. B /\ ph ) ) )
6 3 5 bitr4i 
 |-  ( A. x e. A E* y ( y e. B /\ ph ) <-> A. x E* y ( x e. A /\ ( y e. B /\ ph ) ) )
7 2moswapv 
 |-  ( 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 ) ) ) )
8 df-rmo 
 |-  ( E* x e. A E. y e. B ph <-> E* x ( x e. A /\ E. y e. B ph ) )
9 r19.42v 
 |-  ( E. y e. B ( x e. A /\ ph ) <-> ( x e. A /\ E. y e. B ph ) )
10 df-rex 
 |-  ( E. y e. B ( x e. A /\ ph ) <-> E. y ( y e. B /\ ( x e. A /\ ph ) ) )
11 an12 
 |-  ( ( y e. B /\ ( x e. A /\ ph ) ) <-> ( x e. A /\ ( y e. B /\ ph ) ) )
12 11 exbii 
 |-  ( E. y ( y e. B /\ ( x e. A /\ ph ) ) <-> E. y ( x e. A /\ ( y e. B /\ ph ) ) )
13 10 12 bitri 
 |-  ( E. y e. B ( x e. A /\ ph ) <-> E. y ( x e. A /\ ( y e. B /\ ph ) ) )
14 9 13 bitr3i 
 |-  ( ( x e. A /\ E. y e. B ph ) <-> E. y ( x e. A /\ ( y e. B /\ ph ) ) )
15 14 mobii 
 |-  ( E* x ( x e. A /\ E. y e. B ph ) <-> E* x E. y ( x e. A /\ ( y e. B /\ ph ) ) )
16 8 15 bitri 
 |-  ( E* x e. A E. y e. B ph <-> E* x E. y ( x e. A /\ ( y e. B /\ ph ) ) )
17 df-rmo 
 |-  ( E* y e. B E. x e. A ph <-> E* y ( y e. B /\ E. x e. A ph ) )
18 r19.42v 
 |-  ( E. x e. A ( y e. B /\ ph ) <-> ( y e. B /\ E. x e. A ph ) )
19 df-rex 
 |-  ( E. x e. A ( y e. B /\ ph ) <-> E. x ( x e. A /\ ( y e. B /\ ph ) ) )
20 18 19 bitr3i 
 |-  ( ( y e. B /\ E. x e. A ph ) <-> E. x ( x e. A /\ ( y e. B /\ ph ) ) )
21 20 mobii 
 |-  ( E* y ( y e. B /\ E. x e. A ph ) <-> E* y E. x ( x e. A /\ ( y e. B /\ ph ) ) )
22 17 21 bitri 
 |-  ( E* y e. B E. x e. A ph <-> E* y E. x ( x e. A /\ ( y e. B /\ ph ) ) )
23 7 16 22 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 ) )
24 6 23 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 ) )
25 2 24 sylbi 
 |-  ( A. x e. A E* y e. B ph -> ( E* x e. A E. y e. B ph -> E* y e. B E. x e. A ph ) )