Metamath Proof Explorer

Theorem ralxpf

Description: Version of ralxp with bound-variable hypotheses. (Contributed by NM, 18-Aug-2006) (Revised by Mario Carneiro, 15-Oct-2016)

Ref Expression
Hypotheses ralxpf.1 
|- F/ y ph
ralxpf.2 
|- F/ z ph
ralxpf.3 
|- F/ x ps
ralxpf.4 
|- ( x = <. y , z >. -> ( ph <-> ps ) )
Assertion ralxpf 
|- ( A. x e. ( A X. B ) ph <-> A. y e. A A. z e. B ps )

Proof

Step Hyp Ref Expression
1 ralxpf.1 
 |-  F/ y ph
2 ralxpf.2 
 |-  F/ z ph
3 ralxpf.3 
 |-  F/ x ps
4 ralxpf.4 
 |-  ( x = <. y , z >. -> ( ph <-> ps ) )
5 cbvralsvw 
 |-  ( A. x e. ( A X. B ) ph <-> A. w e. ( A X. B ) [ w / x ] ph )
6 cbvralsvw 
 |-  ( A. z e. B [ u / y ] ps <-> A. v e. B [ v / z ] [ u / y ] ps )
7 6 ralbii 
 |-  ( A. u e. A A. z e. B [ u / y ] ps <-> A. u e. A A. v e. B [ v / z ] [ u / y ] ps )
8 nfv 
 |-  F/ u A. z e. B ps
9 nfcv 
 |-  F/_ y B
10 nfs1v 
 |-  F/ y [ u / y ] ps
11 9 10 nfralw 
 |-  F/ y A. z e. B [ u / y ] ps
12 sbequ12 
 |-  ( y = u -> ( ps <-> [ u / y ] ps ) )
13 12 ralbidv 
 |-  ( y = u -> ( A. z e. B ps <-> A. z e. B [ u / y ] ps ) )
14 8 11 13 cbvralw 
 |-  ( A. y e. A A. z e. B ps <-> A. u e. A A. z e. B [ u / y ] ps )
15 vex 
 |-  u e. _V
16 vex 
 |-  v e. _V
17 15 16 eqvinop 
 |-  ( w = <. u , v >. <-> E. y E. z ( w = <. y , z >. /\ <. y , z >. = <. u , v >. ) )
18 1 nfsbv 
 |-  F/ y [ w / x ] ph
19 10 nfsbv 
 |-  F/ y [ v / z ] [ u / y ] ps
20 18 19 nfbi 
 |-  F/ y ( [ w / x ] ph <-> [ v / z ] [ u / y ] ps )
21 2 nfsbv 
 |-  F/ z [ w / x ] ph
22 nfs1v 
 |-  F/ z [ v / z ] [ u / y ] ps
23 21 22 nfbi 
 |-  F/ z ( [ w / x ] ph <-> [ v / z ] [ u / y ] ps )
24 3 4 sbhypf 
 |-  ( w = <. y , z >. -> ( [ w / x ] ph <-> ps ) )
25 vex 
 |-  y e. _V
26 vex 
 |-  z e. _V
27 25 26 opth 
 |-  ( <. y , z >. = <. u , v >. <-> ( y = u /\ z = v ) )
28 sbequ12 
 |-  ( z = v -> ( [ u / y ] ps <-> [ v / z ] [ u / y ] ps ) )
29 12 28 sylan9bb 
 |-  ( ( y = u /\ z = v ) -> ( ps <-> [ v / z ] [ u / y ] ps ) )
30 27 29 sylbi 
 |-  ( <. y , z >. = <. u , v >. -> ( ps <-> [ v / z ] [ u / y ] ps ) )
31 24 30 sylan9bb 
 |-  ( ( w = <. y , z >. /\ <. y , z >. = <. u , v >. ) -> ( [ w / x ] ph <-> [ v / z ] [ u / y ] ps ) )
32 23 31 exlimi 
 |-  ( E. z ( w = <. y , z >. /\ <. y , z >. = <. u , v >. ) -> ( [ w / x ] ph <-> [ v / z ] [ u / y ] ps ) )
33 20 32 exlimi 
 |-  ( E. y E. z ( w = <. y , z >. /\ <. y , z >. = <. u , v >. ) -> ( [ w / x ] ph <-> [ v / z ] [ u / y ] ps ) )
34 17 33 sylbi 
 |-  ( w = <. u , v >. -> ( [ w / x ] ph <-> [ v / z ] [ u / y ] ps ) )
35 34 ralxp 
 |-  ( A. w e. ( A X. B ) [ w / x ] ph <-> A. u e. A A. v e. B [ v / z ] [ u / y ] ps )
36 7 14 35 3bitr4ri 
 |-  ( A. w e. ( A X. B ) [ w / x ] ph <-> A. y e. A A. z e. B ps )
37 5 36 bitri 
 |-  ( A. x e. ( A X. B ) ph <-> A. y e. A A. z e. B ps )