Metamath Proof Explorer

Theorem 2rexrsb

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

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

Proof

Step Hyp Ref Expression
1 rexrsb 
 |-  ( E. y e. B ph <-> E. w e. B A. y e. B ( 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 e. B ( y = w -> ph ) )
3 rexcom 
 |-  ( E. x e. A E. w e. B A. y e. B ( y = w -> ph ) <-> E. w e. B E. x e. A A. y e. B ( 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 e. B ( y = w -> ph ) )
5 rexrsb 
 |-  ( E. x e. A A. y e. B ( y = w -> ph ) <-> E. z e. A A. x e. A ( x = z -> A. y e. B ( y = w -> ph ) ) )
6 impexp 
 |-  ( ( ( x = z /\ y = w ) -> ph ) <-> ( x = z -> ( y = w -> ph ) ) )
7 6 ralbii 
 |-  ( A. y e. B ( ( x = z /\ y = w ) -> ph ) <-> A. y e. B ( x = z -> ( y = w -> ph ) ) )
8 r19.21v 
 |-  ( A. y e. B ( x = z -> ( y = w -> ph ) ) <-> ( x = z -> A. y e. B ( y = w -> ph ) ) )
9 7 8 bitr2i 
 |-  ( ( x = z -> A. y e. B ( y = w -> ph ) ) <-> A. y e. B ( ( x = z /\ y = w ) -> ph ) )
10 9 ralbii 
 |-  ( A. x e. A ( x = z -> A. y e. B ( y = w -> ph ) ) <-> A. x e. A A. y e. B ( ( x = z /\ y = w ) -> ph ) )
11 10 rexbii 
 |-  ( E. z e. A A. x e. A ( x = z -> A. y e. B ( y = w -> ph ) ) <-> E. z e. A A. x e. A A. y e. B ( ( x = z /\ y = w ) -> ph ) )
12 5 11 bitri 
 |-  ( E. x e. A A. y e. B ( y = w -> ph ) <-> E. z e. A A. x e. A A. y e. B ( ( x = z /\ y = w ) -> ph ) )
13 12 rexbii 
 |-  ( E. w e. B E. x e. A A. y e. B ( y = w -> ph ) <-> E. w e. B E. z e. A A. x e. A A. y e. B ( ( x = z /\ y = w ) -> ph ) )
14 rexcom 
 |-  ( E. w e. B E. z e. A A. x e. A A. y e. B ( ( x = z /\ y = w ) -> ph ) <-> E. z e. A E. w e. B A. x e. A A. y e. B ( ( x = z /\ y = w ) -> ph ) )
15 13 14 bitri 
 |-  ( E. w e. B E. x e. A A. y e. B ( y = w -> ph ) <-> E. z e. A E. w e. B A. x e. A A. y e. B ( ( 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 e. A A. y e. B ( ( x = z /\ y = w ) -> ph ) )