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 )`