Theorem ralxpf 4425

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

Hypotheses

Ref	Expression
ralxpf.1	|- F/yph
ralxpf.2	|- F/zph
ralxpf.3	|- F/xps
ralxpf.4	|- (x = <.y , z >. -> (ph <-> ps))

Assertion

Ref	Expression
ralxpf	|- (A.x e. (A X. B)ph <-> A.y e. A A.z e. B ps)

Distinct variable groups:   x,y,A   x,z,B,y

Allowed substitution hints:   ph(x,y,z)   ps(x,y,z)   A(z)

Proof of Theorem ralxpf

Dummy variables v u w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cbvralsv 2538	. 2 |- (A.x e. (A X. B)ph <-> A.v e. (A X. B)[v / x]ph)
2		cbvralsv 2538	. . . 4 |- (A.z e. B [w / y]ps <-> A.u e. B [u / z][w / y]ps)
3	2	ralbii 2324	. . 3 |- (A.w e. A A.z e. B [w / y]ps <-> A.w e. A A.u e. B [u / z][w / y]ps)
4		nfv 1418	. . . 4 |- F/wA.z e. B ps
5		nfcv 2175	. . . . 5 |- F/_yB
6		nfs1v 1812	. . . . 5 |- F/y[w / y]ps
7	5, 6	nfralxy 2354	. . . 4 |- F/yA.z e. B [w / y]ps
8		sbequ12 1651	. . . . 5 |- (y = w -> (ps <-> [w / y]ps))
9	8	ralbidv 2320	. . . 4 |- (y = w -> (A.z e. B ps <-> A.z e. B [w / y]ps))
10	4, 7, 9	cbvral 2523	. . 3 |- (A.y e. A A.z e. B ps <-> A.w e. A A.z e. B [w / y]ps)
11		vex 2554	. . . . . 6 |- w e. _V
12		vex 2554	. . . . . 6 |- u e. _V
13	11, 12	eqvinop 3971	. . . . 5 |- (v = <.w , u >. <-> E.yE.z(v = <.y , z >. /\ <.y , z >. = <.w , u >.))
14		ralxpf.1	. . . . . . . 8 |- F/yph
15	14	nfsb 1819	. . . . . . 7 |- F/y[v / x]ph
16	6	nfsb 1819	. . . . . . 7 |- F/y[u / z][w / y]ps
17	15, 16	nfbi 1478	. . . . . 6 |- F/y([v / x]ph <-> [u / z][w / y]ps)
18		ralxpf.2	. . . . . . . . 9 |- F/zph
19	18	nfsb 1819	. . . . . . . 8 |- F/z[v / x]ph
20		nfs1v 1812	. . . . . . . 8 |- F/z[u / z][w / y]ps
21	19, 20	nfbi 1478	. . . . . . 7 |- F/z([v / x]ph <-> [u / z][w / y]ps)
22		ralxpf.3	. . . . . . . . 9 |- F/xps
23		ralxpf.4	. . . . . . . . 9 |- (x = <.y , z >. -> (ph <-> ps))
24	22, 23	sbhypf 2597	. . . . . . . 8 |- (v = <.y , z >. -> ([v / x]ph <-> ps))
25		vex 2554	. . . . . . . . . 10 |- y e. _V
26		vex 2554	. . . . . . . . . 10 |- z e. _V
27	25, 26	opth 3965	. . . . . . . . 9 |- ( <.y , z >. = <.w , u >. <-> (y = w /\ z = u))
28		sbequ12 1651	. . . . . . . . . 10 |- (z = u -> ([w / y]ps <-> [u / z][w / y]ps))
29	8, 28	sylan9bb 435	. . . . . . . . 9 |- ((y = w /\ z = u) -> (ps <-> [u / z][w / y]ps))
30	27, 29	sylbi 114	. . . . . . . 8 |- ( <.y , z >. = <.w , u >. -> (ps <-> [u / z][w / y]ps))
31	24, 30	sylan9bb 435	. . . . . . 7 |- ((v = <.y , z >. /\ <.y , z >. = <.w , u >.) -> ([v / x]ph <-> [u / z][w / y]ps))
32	21, 31	exlimi 1482	. . . . . 6 |- (E.z(v = <.y , z >. /\ <.y , z >. = <.w , u >.) -> ([v / x]ph <-> [u / z][w / y]ps))
33	17, 32	exlimi 1482	. . . . 5 |- (E.yE.z(v = <.y , z >. /\ <.y , z >. = <.w , u >.) -> ([v / x]ph <-> [u / z][w / y]ps))
34	13, 33	sylbi 114	. . . 4 |- (v = <.w , u >. -> ([v / x]ph <-> [u / z][w / y]ps))
35	34	ralxp 4422	. . 3 |- (A.v e. (A X. B)[v / x]ph <-> A.w e. A A.u e. B [u / z][w / y]ps)
36	3, 10, 35	3bitr4ri 202	. 2 |- (A.v e. (A X. B)[v / x]ph <-> A.y e. A A.z e. B ps)
37	1, 36	bitri 173	1 |- (A.x e. (A X. B)ph <-> A.y e. A A.z e. B ps)

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98   = wceq 1242   F/wnf 1346  E.wex 1378  [wsb 1642  A.wral 2300   <.cop 3370   X. cxp 4286

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-sbc 2759  df-csb 2847  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-iun 3650  df-opab 3810  df-xp 4294  df-rel 4295

This theorem is referenced by: (None)