Theorem ralxpf 3210

Description: Version of ralxp 3208 with bound-variable hypotheses.

Hypotheses

Ref	Expression
ralxpf.1	|- (ph -> A.yph)
ralxpf.2	|- (ph -> A.zph)
ralxpf.3	|- (ps -> A.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

Proof of Theorem ralxpf

Step	Hyp	Ref	Expression
1		cbvralsv 1957	. 2 |- (A.x e. (A X. B)ph <-> A.w e. (A X. B)[w / x]ph)
2		cbvralsv 1957	. . . 4 |- (A.z e. B [u / y]ps <-> A.v e. B [v / z][u / y]ps)
3	2	ralbii 1659	. . 3 |- (A.u e. A A.z e. B [u / y]ps <-> A.u e. A A.v e. B [v / z][u / y]ps)
4		ax-17 968	. . . 4 |- (A.z e. B ps -> A.uA.z e. B ps)
5		ax-17 968	. . . . 5 |- (z e. B -> A.y z e. B)
6		hbs1 1327	. . . . 5 |- ([u / y]ps -> A.y[u / y]ps)
7	5, 6	hbral 1678	. . . 4 |- (A.z e. B [u / y]ps -> A.yA.z e. B [u / y]ps)
8		sbequ12 1177	. . . . 5 |- (y = u -> (ps <-> [u / y]ps))
9	8	ralbidv 1655	. . . 4 |- (y = u -> (A.z e. B ps <-> A.z e. B [u / y]ps))
10	4, 7, 9	cbvral 1789	. . 3 |- (A.y e. A A.z e. B ps <-> A.u e. A A.z e. B [u / y]ps)
11		visset 1804	. . . . . 6 |- u e. V
12		visset 1804	. . . . . 6 |- v e. V
13	11, 12	eqvinop 2781	. . . . 5 |- (w = <.u, v>. <-> E.yE.z(w = <.y, z>. /\ <.y, z>. = <.u, v>.))
14		visset 1804	. . . . . . . 8 |- w e. V
15		ax-17 968	. . . . . . . . 9 |- (x e. w -> A.y x e. w)
16		ralxpf.1	. . . . . . . . 9 |- (ph -> A.yph)
17	15, 16	hbsbcg 1941	. . . . . . . 8 |- (w e. V -> ([w / x]ph -> A.y[w / x]ph))
18	14, 17	ax-mp 7	. . . . . . 7 |- ([w / x]ph -> A.y[w / x]ph)
19		ax-17 968	. . . . . . . . 9 |- (x e. v -> A.y x e. v)
20	19, 6	hbsbcg 1941	. . . . . . . 8 |- (v e. V -> ([v / z][u / y]ps -> A.y[v / z][u / y]ps))
21	12, 20	ax-mp 7	. . . . . . 7 |- ([v / z][u / y]ps -> A.y[v / z][u / y]ps)
22	18, 21	hbbi 1007	. . . . . 6 |- (([w / x]ph <-> [v / z][u / y]ps) -> A.y([w / x]ph <-> [v / z][u / y]ps))
23		ax-17 968	. . . . . . . . . 10 |- (x e. w -> A.z x e. w)
24		ralxpf.2	. . . . . . . . . 10 |- (ph -> A.zph)
25	23, 24	hbsbcg 1941	. . . . . . . . 9 |- (w e. V -> ([w / x]ph -> A.z[w / x]ph))
26	14, 25	ax-mp 7	. . . . . . . 8 |- ([w / x]ph -> A.z[w / x]ph)
27		hbs1 1327	. . . . . . . 8 |- ([v / z][u / y]ps -> A.z[v / z][u / y]ps)
28	26, 27	hbbi 1007	. . . . . . 7 |- (([w / x]ph <-> [v / z][u / y]ps) -> A.z([w / x]ph <-> [v / z][u / y]ps))
29	14	eqvinc 1874	. . . . . . . . 9 |- (w = <.y, z>. <-> E.x(x = w /\ x = <.y, z>.))
30		hbs1 1327	. . . . . . . . . . 11 |- ([w / x]ph -> A.x[w / x]ph)
31		ralxpf.3	. . . . . . . . . . 11 |- (ps -> A.xps)
32	30, 31	hbbi 1007	. . . . . . . . . 10 |- (([w / x]ph <-> ps) -> A.x([w / x]ph <-> ps))
33		sbequ12 1177	. . . . . . . . . . . 12 |- (x = w -> (ph <-> [w / x]ph))
34	33	bicomd 519	. . . . . . . . . . 11 |- (x = w -> ([w / x]ph <-> ph))
35		ralxpf.4	. . . . . . . . . . 11 |- (x = <.y, z>. -> (ph <-> ps))
36	34, 35	sylan9bb 538	. . . . . . . . . 10 |- ((x = w /\ x = <.y, z>.) -> ([w / x]ph <-> ps))
37	32, 36	19.23ai 1060	. . . . . . . . 9 |- (E.x(x = w /\ x = <.y, z>.) -> ([w / x]ph <-> ps))
38	29, 37	sylbi 199	. . . . . . . 8 |- (w = <.y, z>. -> ([w / x]ph <-> ps))
39		visset 1804	. . . . . . . . . 10 |- y e. V
40		visset 1804	. . . . . . . . . 10 |- z e. V
41	39, 40, 12	opth 2777	. . . . . . . . 9 |- (<.y, z>. = <.u, v>. <-> (y = u /\ z = v))
42		sbequ12 1177	. . . . . . . . . 10 |- (z = v -> ([u / y]ps <-> [v / z][u / y]ps))
43	8, 42	sylan9bb 538	. . . . . . . . 9 |- ((y = u /\ z = v) -> (ps <-> [v / z][u / y]ps))
44	41, 43	sylbi 199	. . . . . . . 8 |- (<.y, z>. = <.u, v>. -> (ps <-> [v / z][u / y]ps))
45	38, 44	sylan9bb 538	. . . . . . 7 |- ((w = <.y, z>. /\ <.y, z>. = <.u, v>.) -> ([w / x]ph <-> [v / z][u / y]ps))
46	28, 45	19.23ai 1060	. . . . . 6 |- (E.z(w = <.y, z>. /\ <.y, z>. = <.u, v>.) -> ([w / x]ph <-> [v / z][u / y]ps))
47	22, 46	19.23ai 1060	. . . . 5 |- (E.yE.z(w = <.y, z>. /\ <.y, z>. = <.u, v>.) -> ([w / x]ph <-> [v / z][u / y]ps))
48	13, 47	sylbi 199	. . . 4 |- (w = <.u, v>. -> ([w / x]ph <-> [v / z][u / y]ps))
49	48	ralxp 3208	. . 3 |- (A.w e. (A X. B)[w / x]ph <-> A.u e. A A.v e. B [v / z][u / y]ps)
50	3, 10, 49	3bitr4r 184	. 2 |- (A.w e. (A X. B)[w / x]ph <-> A.y e. A A.z e. B ps)
51	1, 50	bitr 173	1 |- (A.x e. (A X. B)ph <-> A.y e. A A.z e. B ps)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223  A.wal 951   = wceq 953   e. wcel 955  E.wex 977  [wsbc 1166  A.wral 1637  Vcvv 1802  <.cop 2401   X. cxp 3158

This theorem is referenced by:  foprab2 4103

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-pow 2732  ax-pr 2769

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-ral 1641  df-v 1803  df-sbc 1932  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-opab 2657  df-xp 3174

Copyright terms: Public domain