Metamath Proof Explorer

Theorem ralxpxfr2d

Description: Transfer a universal quantifier between one variable with pair-like semantics and two. (Contributed by Stefan O'Rear, 27-Feb-2015)

Ref Expression
Hypotheses ralxpxfr2d.a 
|- A e. _V
ralxpxfr2d.b 
|- ( ph -> ( x e. B <-> E. y e. C E. z e. D x = A ) )
ralxpxfr2d.c 
|- ( ( ph /\ x = A ) -> ( ps <-> ch ) )
Assertion ralxpxfr2d 
|- ( ph -> ( A. x e. B ps <-> A. y e. C A. z e. D ch ) )

Proof

Step Hyp Ref Expression
1 ralxpxfr2d.a 
 |-  A e. _V
2 ralxpxfr2d.b 
 |-  ( ph -> ( x e. B <-> E. y e. C E. z e. D x = A ) )
3 ralxpxfr2d.c 
 |-  ( ( ph /\ x = A ) -> ( ps <-> ch ) )
4 df-ral 
 |-  ( A. x e. B ps <-> A. x ( x e. B -> ps ) )
5 2 imbi1d 
 |-  ( ph -> ( ( x e. B -> ps ) <-> ( E. y e. C E. z e. D x = A -> ps ) ) )
6 5 albidv 
 |-  ( ph -> ( A. x ( x e. B -> ps ) <-> A. x ( E. y e. C E. z e. D x = A -> ps ) ) )
7 4 6 bitrid 
 |-  ( ph -> ( A. x e. B ps <-> A. x ( E. y e. C E. z e. D x = A -> ps ) ) )
8 ralcom4 
 |-  ( A. y e. C A. x A. z e. D ( x = A -> ps ) <-> A. x A. y e. C A. z e. D ( x = A -> ps ) )
9 ralcom4 
 |-  ( A. z e. D A. x ( x = A -> ps ) <-> A. x A. z e. D ( x = A -> ps ) )
10 9 ralbii 
 |-  ( A. y e. C A. z e. D A. x ( x = A -> ps ) <-> A. y e. C A. x A. z e. D ( x = A -> ps ) )
11 r19.23v 
 |-  ( A. z e. D ( x = A -> ps ) <-> ( E. z e. D x = A -> ps ) )
12 11 ralbii 
 |-  ( A. y e. C A. z e. D ( x = A -> ps ) <-> A. y e. C ( E. z e. D x = A -> ps ) )
13 r19.23v 
 |-  ( A. y e. C ( E. z e. D x = A -> ps ) <-> ( E. y e. C E. z e. D x = A -> ps ) )
14 12 13 bitr2i 
 |-  ( ( E. y e. C E. z e. D x = A -> ps ) <-> A. y e. C A. z e. D ( x = A -> ps ) )
15 14 albii 
 |-  ( A. x ( E. y e. C E. z e. D x = A -> ps ) <-> A. x A. y e. C A. z e. D ( x = A -> ps ) )
16 8 10 15 3bitr4ri 
 |-  ( A. x ( E. y e. C E. z e. D x = A -> ps ) <-> A. y e. C A. z e. D A. x ( x = A -> ps ) )
17 7 16 bitrdi 
 |-  ( ph -> ( A. x e. B ps <-> A. y e. C A. z e. D A. x ( x = A -> ps ) ) )
18 3 pm5.74da 
 |-  ( ph -> ( ( x = A -> ps ) <-> ( x = A -> ch ) ) )
19 18 albidv 
 |-  ( ph -> ( A. x ( x = A -> ps ) <-> A. x ( x = A -> ch ) ) )
20 biidd 
 |-  ( x = A -> ( ch <-> ch ) )
21 1 20 ceqsalv 
 |-  ( A. x ( x = A -> ch ) <-> ch )
22 19 21 bitrdi 
 |-  ( ph -> ( A. x ( x = A -> ps ) <-> ch ) )
23 22 2ralbidv 
 |-  ( ph -> ( A. y e. C A. z e. D A. x ( x = A -> ps ) <-> A. y e. C A. z e. D ch ) )
24 17 23 bitrd 
 |-  ( ph -> ( A. x e. B ps <-> A. y e. C A. z e. D ch ) )