Metamath Proof Explorer

Theorem 2rexsb

Description: An equivalent expression for double restricted existence, analogous to rexsb . (Contributed by Alexander van der Vekens, 1-Jul-2017)

Ref Expression
Assertion 2rexsb 
|- ( E. x e. A E. y e. B ph <-> E. z e. A E. w e. B A. x A. y ( ( x = z /\ y = w ) -> ph ) )

Proof

Step Hyp Ref Expression
1 rexsb 
 |-  ( E. y e. B ph <-> E. w e. B A. y ( y = w -> ph ) )
2 1 rexbii 
 |-  ( E. x e. A E. y e. B ph <-> E. x e. A E. w e. B A. y ( y = w -> ph ) )
3 rexcom 
 |-  ( E. x e. A E. w e. B A. y ( y = w -> ph ) <-> E. w e. B E. x e. A A. y ( y = w -> ph ) )
4 2 3 bitri 
 |-  ( E. x e. A E. y e. B ph <-> E. w e. B E. x e. A A. y ( y = w -> ph ) )
5 rexsb 
 |-  ( E. x e. A A. y ( y = w -> ph ) <-> E. z e. A A. x ( x = z -> A. y ( y = w -> ph ) ) )
6 impexp 
 |-  ( ( ( x = z /\ y = w ) -> ph ) <-> ( x = z -> ( y = w -> ph ) ) )
7 6 albii 
 |-  ( A. y ( ( x = z /\ y = w ) -> ph ) <-> A. y ( x = z -> ( y = w -> ph ) ) )
8 19.21v 
 |-  ( A. y ( x = z -> ( y = w -> ph ) ) <-> ( x = z -> A. y ( y = w -> ph ) ) )
9 7 8 bitr2i 
 |-  ( ( x = z -> A. y ( y = w -> ph ) ) <-> A. y ( ( x = z /\ y = w ) -> ph ) )
10 9 albii 
 |-  ( A. x ( x = z -> A. y ( y = w -> ph ) ) <-> A. x A. y ( ( x = z /\ y = w ) -> ph ) )
11 10 rexbii 
 |-  ( E. z e. A A. x ( x = z -> A. y ( y = w -> ph ) ) <-> E. z e. A A. x A. y ( ( x = z /\ y = w ) -> ph ) )
12 5 11 bitri 
 |-  ( E. x e. A A. y ( y = w -> ph ) <-> E. z e. A A. x A. y ( ( x = z /\ y = w ) -> ph ) )
13 12 rexbii 
 |-  ( E. w e. B E. x e. A A. y ( y = w -> ph ) <-> E. w e. B E. z e. A A. x A. y ( ( x = z /\ y = w ) -> ph ) )
14 rexcom 
 |-  ( E. w e. B E. z e. A A. x A. y ( ( x = z /\ y = w ) -> ph ) <-> E. z e. A E. w e. B A. x A. y ( ( x = z /\ y = w ) -> ph ) )
15 13 14 bitri 
 |-  ( E. w e. B E. x e. A A. y ( y = w -> ph ) <-> E. z e. A E. w e. B A. x A. y ( ( x = z /\ y = w ) -> ph ) )
16 4 15 bitri 
 |-  ( E. x e. A E. y e. B ph <-> E. z e. A E. w e. B A. x A. y ( ( x = z /\ y = w ) -> ph ) )