Theorem ralxpf 3220

Description: Version of ralxp 3218 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 1967	. 2 |- (A.x e. (A X. B)ph <-> A.w e. (A X. B)[w / x]ph)
2		cbvralsv 1967	. . . 4 |- (A.z e. B [u / y]ps <-> A.v e. B [v / z][u / y]ps)
3	2	ralbii 1667	. . 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 971	. . . 4 |- (A.z e. B ps -> A.uA.z e. B ps)
5		ax-17 971	. . . . 5 |- (z e. B -> A.y z e. B)
6		hbs1 1332	. . . . 5 |- ([u / y]ps -> A.y[u / y]ps)
7	5, 6	hbral 1686	. . . 4 |- (A.z e. B [u / y]ps -> A.yA.z e. B [u / y]ps)
8		sbequ12 1181	. . . . 5 |- (y = u -> (ps <-> [u / y]ps))
9	8	ralbidv 1663	. . . 4 |- (y = u -> (A.z e. B ps <-> A.z e. B [u / y]ps))
10	4, 7, 9	cbvral 1798	. . 3 |- (A.y e. A A.z e. B ps <-> A.u e. A A.z e. B [u / y]ps)
11		visset 1813	. . . . . 6 |- u e. V
12		visset 1813	. . . . . 6 |- v e. V
13	11, 12	eqvinop 2791	. . . . 5 |- (w = <.u, v>. <-> E.yE.z(w = <.y, z>. /\ <.y, z>. = <.u, v>.))
14		visset 1813	. . . . . . . 8 |- w e. V
15		ax-17 971	. . . . . . . . 9 |- (x e. w -> A.y x e. w)
16		ralxpf.1	. . . . . . . . 9 |- (ph -> A.yph)
17	15, 16	hbsbcg 1951	. . . . . . . 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 971	. . . . . . . . 9 |- (x e. v -> A.y x e. v)
20	19, 6	hbsbcg 1951	. . . . . . . 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 1010	. . . . . 6 |- (([w / x]ph <-> [v / z][u / y]ps) -> A.y([w / x]ph <-> [v / z][u / y]ps))
23		ax-17 971	. . . . . . . . . 10 |- (x e. w -> A.z x e. w)
24		ralxpf.2	. . . . . . . . . 10 |- (ph -> A.zph)
25	23, 24	hbsbcg 1951	. . . . . . . . 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 1332	. . . . . . . 8 |- ([v / z][u / y]ps -> A.z[v / z][u / y]ps)
28	26, 27	hbbi 1010	. . . . . . 7 |- (([w / x]ph <-> [v / z][u / y]ps) -> A.z([w / x]ph <-> [v / z][u / y]ps))
29	14	eqvinc 1883	. . . . . . . . 9 |- (w = <.y, z>. <-> E.x(x = w /\ x = <.y, z>.))
30		hbs1 1332	. . . . . . . . . . 11 |- ([w / x]ph -> A.x[w / x]ph)
31		ralxpf.3	. . . . . . . . . . 11 |- (ps -> A.xps)
32	30, 31	hbbi 1010	. . . . . . . . . 10 |- (([w / x]ph <-> ps) -> A.x([w / x]ph <-> ps))
33		sbequ12 1181	. . . . . . . . . . . 12 |- (x = w -> (ph <-> [w / x]ph))
34	33	bicomd 521	. . . . . . . . . . 11 |- (x = w -> ([w / x]ph <-> ph))
35		ralxpf.4	. . . . . . . . . . 11 |- (x = <.y, z>. -> (ph <-> ps))
36	34, 35	sylan9bb 540	. . . . . . . . . 10 |- ((x = w /\ x = <.y, z>.) -> ([w / x]ph <-> ps))
37	32, 36	19.23ai 1064	. . . . . . . . 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 1813	. . . . . . . . . 10 |- y e. V
40		visset 1813	. . . . . . . . . 10 |- z e. V
41	39, 40, 12	opth 2787	. . . . . . . . 9 |- (<.y, z>. = <.u, v>. <-> (y = u /\ z = v))
42		sbequ12 1181	. . . . . . . . . 10 |- (z = v -> ([u / y]ps <-> [v / z][u / y]ps))
43	8, 42	sylan9bb 540	. . . . . . . . 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 540	. . . . . . 7 |- ((w = <.y, z>. /\ <.y, z>. = <.u, v>.) -> ([w / x]ph <-> [v / z][u / y]ps))
46	28, 45	19.23ai 1064	. . . . . 6 |- (E.z(w = <.y, z>. /\ <.y, z>. = <.u, v>.) -> ([w / x]ph <-> [v / z][u / y]ps))
47	22, 46	19.23ai 1064	. . . . 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 3218	. . 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 954   = wceq 956   e. wcel 958  E.wex 980  [wsbc 1170  A.wral 1645  Vcvv 1811  <.cop 2411   X. cxp 3168

This theorem is referenced by:  foprab2 4119

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-9 965  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-pow 2742  ax-pr 2779

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-ral 1649  df-v 1812  df-sbc 1942  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-opab 2667  df-xp 3184

Copyright terms: Public domain