Theorem sbcralt 1980

Description: Interchange class substitution and restricted quantifier.

Assertion

Ref	Expression
sbcralt	|- (A.y(A e. C /\ A.z(z e. A -> A.y z e. A)) -> ([A / x]A.y e. B ph <-> A.y e. B [A / x]ph))

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

Proof of Theorem sbcralt

Step	Hyp	Ref	Expression
1		sbc6g 1945	. . . . . 6 |- (A e. C -> ([A / w]A.y e. B [w / x]ph <-> A.w(w = A -> A.y e. B [w / x]ph)))
2	1	adantr 389	. . . . 5 |- ((A e. C /\ A.z(z e. A -> A.y z e. A)) -> ([A / w]A.y e. B [w / x]ph <-> A.w(w = A -> A.y e. B [w / x]ph)))
3	2	a4s 981	. . . 4 |- (A.y(A e. C /\ A.z(z e. A -> A.y z e. A)) -> ([A / w]A.y e. B [w / x]ph <-> A.w(w = A -> A.y e. B [w / x]ph)))
4		hba1 1000	. . . . . . . . 9 |- (A.y(A e. C /\ A.z(z e. A -> A.y z e. A)) -> A.yA.y(A e. C /\ A.z(z e. A -> A.y z e. A)))
5		ax-17 968	. . . . . . . . . 10 |- (v e. w -> A.y v e. w)
6	5	a1i 8	. . . . . . . . 9 |- (A.y(A e. C /\ A.z(z e. A -> A.y z e. A)) -> (v e. w -> A.y v e. w))
7		eleq1 1526	. . . . . . . . . . . . 13 |- (z = v -> (z e. A <-> v e. A))
8	7	albidv 1273	. . . . . . . . . . . . 13 |- (z = v -> (A.y z e. A <-> A.y v e. A))
9	7, 8	imbi12d 624	. . . . . . . . . . . 12 |- (z = v -> ((z e. A -> A.y z e. A) <-> (v e. A -> A.y v e. A)))
10	9	a4v 1267	. . . . . . . . . . 11 |- (A.z(z e. A -> A.y z e. A) -> (v e. A -> A.y v e. A))
11	10	adantl 388	. . . . . . . . . 10 |- ((A e. C /\ A.z(z e. A -> A.y z e. A)) -> (v e. A -> A.y v e. A))
12	11	a4s 981	. . . . . . . . 9 |- (A.y(A e. C /\ A.z(z e. A -> A.y z e. A)) -> (v e. A -> A.y v e. A))
13	4, 6, 12	hbeqd 1904	. . . . . . . 8 |- (A.y(A e. C /\ A.z(z e. A -> A.y z e. A)) -> (w = A -> A.y w = A))
14	13	a5i 986	. . . . . . 7 |- (A.y(A e. C /\ A.z(z e. A -> A.y z e. A)) -> A.y(w = A -> A.y w = A))
15		r19.21t 1707	. . . . . . 7 |- (A.y(w = A -> A.y w = A) -> (A.y e. B (w = A -> [w / x]ph) <-> (w = A -> A.y e. B [w / x]ph)))
16	14, 15	syl 10	. . . . . 6 |- (A.y(A e. C /\ A.z(z e. A -> A.y z e. A)) -> (A.y e. B (w = A -> [w / x]ph) <-> (w = A -> A.y e. B [w / x]ph)))
17	16	albidv 1273	. . . . 5 |- (A.y(A e. C /\ A.z(z e. A -> A.y z e. A)) -> (A.wA.y e. B (w = A -> [w / x]ph) <-> A.w(w = A -> A.y e. B [w / x]ph)))
18		ralcom4 1814	. . . . 5 |- (A.y e. B A.w(w = A -> [w / x]ph) <-> A.wA.y e. B (w = A -> [w / x]ph))
19	17, 18	syl5rbb 531	. . . 4 |- (A.y(A e. C /\ A.z(z e. A -> A.y z e. A)) -> (A.w(w = A -> A.y e. B [w / x]ph) <-> A.y e. B A.w(w = A -> [w / x]ph)))
20	3, 19	bitrd 526	. . 3 |- (A.y(A e. C /\ A.z(z e. A -> A.y z e. A)) -> ([A / w]A.y e. B [w / x]ph <-> A.y e. B A.w(w = A -> [w / x]ph)))
21		visset 1804	. . . . . . 7 |- w e. V
22		sbc6g 1945	. . . . . . . . 9 |- (w e. V -> ([w / x]A.y e. B ph <-> A.x(x = w -> A.y e. B ph)))
23		ralcom4 1814	. . . . . . . . . 10 |- (A.y e. B A.x(x = w -> ph) <-> A.xA.y e. B (x = w -> ph))
24		r19.21v 1708	. . . . . . . . . . 11 |- (A.y e. B (x = w -> ph) <-> (x = w -> A.y e. B ph))
25	24	albii 996	. . . . . . . . . 10 |- (A.xA.y e. B (x = w -> ph) <-> A.x(x = w -> A.y e. B ph))
26	23, 25	bitr2 174	. . . . . . . . 9 |- (A.x(x = w -> A.y e. B ph) <-> A.y e. B A.x(x = w -> ph))
27	22, 26	syl6bb 534	. . . . . . . 8 |- (w e. V -> ([w / x]A.y e. B ph <-> A.y e. B A.x(x = w -> ph)))
28		sbc6g 1945	. . . . . . . . 9 |- (w e. V -> ([w / x]ph <-> A.x(x = w -> ph)))
29	28	ralbidv 1655	. . . . . . . 8 |- (w e. V -> (A.y e. B [w / x]ph <-> A.y e. B A.x(x = w -> ph)))
30	27, 29	bitr4d 529	. . . . . . 7 |- (w e. V -> ([w / x]A.y e. B ph <-> A.y e. B [w / x]ph))
31	21, 30	ax-mp 7	. . . . . 6 |- ([w / x]A.y e. B ph <-> A.y e. B [w / x]ph)
32	31	sbcbii 1968	. . . . 5 |- (A e. C -> ([A / w][w / x]A.y e. B ph <-> [A / w]A.y e. B [w / x]ph))
33	32	adantr 389	. . . 4 |- ((A e. C /\ A.z(z e. A -> A.y z e. A)) -> ([A / w][w / x]A.y e. B ph <-> [A / w]A.y e. B [w / x]ph))
34	33	a4s 981	. . 3 |- (A.y(A e. C /\ A.z(z e. A -> A.y z e. A)) -> ([A / w][w / x]A.y e. B ph <-> [A / w]A.y e. B [w / x]ph))
35		sbc6g 1945	. . . . . 6 |- (A e. C -> ([A / w][w / x]ph <-> A.w(w = A -> [w / x]ph)))
36	35	adantr 389	. . . . 5 |- ((A e. C /\ A.z(z e. A -> A.y z e. A)) -> ([A / w][w / x]ph <-> A.w(w = A -> [w / x]ph)))
37	36	a4s 981	. . . 4 |- (A.y(A e. C /\ A.z(z e. A -> A.y z e. A)) -> ([A / w][w / x]ph <-> A.w(w = A -> [w / x]ph)))
38	4, 37	ralbid 1653	. . 3 |- (A.y(A e. C /\ A.z(z e. A -> A.y z e. A)) -> (A.y e. B [A / w][w / x]ph <-> A.y e. B A.w(w = A -> [w / x]ph)))
39	20, 34, 38	3bitr4d 548	. 2 |- (A.y(A e. C /\ A.z(z e. A -> A.y z e. A)) -> ([A / w][w / x]A.y e. B ph <-> A.y e. B [A / w][w / x]ph))
40		sbccog 1942	. . . 4 |- (A e. C -> ([A / w][w / x]A.y e. B ph <-> [A / x]A.y e. B ph))
41	40	adantr 389	. . 3 |- ((A e. C /\ A.z(z e. A -> A.y z e. A)) -> ([A / w][w / x]A.y e. B ph <-> [A / x]A.y e. B ph))
42	41	a4s 981	. 2 |- (A.y(A e. C /\ A.z(z e. A -> A.y z e. A)) -> ([A / w][w / x]A.y e. B ph <-> [A / x]A.y e. B ph))
43		sbccog 1942	. . . . 5 |- (A e. C -> ([A / w][w / x]ph <-> [A / x]ph))
44	43	adantr 389	. . . 4 |- ((A e. C /\ A.z(z e. A -> A.y z e. A)) -> ([A / w][w / x]ph <-> [A / x]ph))
45	44	a4s 981	. . 3 |- (A.y(A e. C /\ A.z(z e. A -> A.y z e. A)) -> ([A / w][w / x]ph <-> [A / x]ph))
46	4, 45	ralbid 1653	. 2 |- (A.y(A e. C /\ A.z(z e. A -> A.y z e. A)) -> (A.y e. B [A / w][w / x]ph <-> A.y e. B [A / x]ph))
47	39, 42, 46	3bitr3d 546	1 |- (A.y(A e. C /\ A.z(z e. A -> A.y z e. A)) -> ([A / x]A.y e. B ph <-> A.y e. B [A / x]ph))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223  A.wal 951   = wceq 953   e. wcel 955  [wsbc 1166  A.wral 1637  Vcvv 1802

This theorem is referenced by:  sbcrext 1981  sbcralg 1984

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

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465