Theorem sbcralt 2360

Description: Interchange class substitution and restricted quantifier. (Unnecessary distinct variable restrictions were removed by David Abernethy, 22-Feb-2010.)

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   x,y   y,z

Proof of Theorem sbcralt

Step	Hyp	Ref	Expression
1		sbc6g 2305	. . . . . 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 423	. . . . 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 1168	. . . 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 1188	. . . . . . . . 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 1155	. . . . . . . . . 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 1794	. . . . . . . . . . . . 13 |- (z = v -> (z e. A <-> v e. A))
8	7	albidv 1494	. . . . . . . . . . . . 13 |- (z = v -> (A.y z e. A <-> A.y v e. A))
9	7, 8	imbi12d 685	. . . . . . . . . . . 12 |- (z = v -> ((z e. A -> A.y z e. A) <-> (v e. A -> A.y v e. A)))
10	9	a4v 1487	. . . . . . . . . . 11 |- (A.z(z e. A -> A.y z e. A) -> (v e. A -> A.y v e. A))
11	10	adantl 422	. . . . . . . . . 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 1168	. . . . . . . . 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 2257	. . . . . . . 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 1173	. . . . . . 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 2011	. . . . . . 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 12	. . . . . 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 1494	. . . . 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 2143	. . . . 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 589	. . . 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 584	. . 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 2128	. . . . . . 7 |- w e. _V
22		sbc6g 2305	. . . . . . . . 9 |- (w e. _V -> ([w / x]A.y e. B ph <-> A.x(x = w -> A.y e. B ph)))
23		ralcom4 2143	. . . . . . . . . 10 |- (A.y e. B A.x(x = w -> ph) <-> A.xA.y e. B (x = w -> ph))
24		r19.21v 2012	. . . . . . . . . . 11 |- (A.y e. B (x = w -> ph) <-> (x = w -> A.y e. B ph))
25	24	albii 1184	. . . . . . . . . 10 |- (A.xA.y e. B (x = w -> ph) <-> A.x(x = w -> A.y e. B ph))
26	23, 25	bitr2i 190	. . . . . . . . 9 |- (A.x(x = w -> A.y e. B ph) <-> A.y e. B A.x(x = w -> ph))
27	22, 26	syl6bb 592	. . . . . . . 8 |- (w e. _V -> ([w / x]A.y e. B ph <-> A.y e. B A.x(x = w -> ph)))
28		sbc6g 2305	. . . . . . . . 9 |- (w e. _V -> ([w / x]ph <-> A.x(x = w -> ph)))
29	28	ralbidv 1957	. . . . . . . 8 |- (w e. _V -> (A.y e. B [w / x]ph <-> A.y e. B A.x(x = w -> ph)))
30	27, 29	bitr4d 587	. . . . . . 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 2339	. . . . 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 423	. . . 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 1168	. . 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 2305	. . . . . 6 |- (A e. C -> ([A / w][w / x]ph <-> A.w(w = A -> [w / x]ph)))
36	35	adantr 423	. . . . 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 1168	. . . 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 1955	. . 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 606	. 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 2300	. . . 4 |- (A e. C -> ([A / w][w / x]A.y e. B ph <-> [A / x]A.y e. B ph))
41	40	adantr 423	. . 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 1168	. 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 2300	. . . . 5 |- (A e. C -> ([A / w][w / x]ph <-> [A / x]ph))
44	43	adantr 423	. . . 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 1168	. . 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 1955	. 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 604	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 162   /\ wa 239  A.wal 1134   = wceq 1136   e. wcel 1138  [wsbc 1372  A.wral 1939  _Vcvv 2125

This theorem is referenced by:  sbcrext 2361  sbcralgOLD 2365

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1140  ax-7 1142  ax-gen 1143  ax-8 1144  ax-9 1145  ax-10 1146  ax-11 1147  ax-12 1148  ax-17 1155  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319  ax-10o 1338  ax-16 1418  ax-11o 1426  ax-ext 1702

This theorem depends on definitions:  df-bi 163  df-or 240  df-an 241  df-ex 1165  df-sb 1374  df-clab 1709  df-cleq 1714  df-clel 1717  df-ral 1943  df-v 2127  df-sbc 2287

Copyright terms: Public domain