Theorem sbcralt 2000

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 1962	. . . . . 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 391	. . . . 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 988	. . . 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 1007	. . . . . . . . 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 975	. . . . . . . . . 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 1541	. . . . . . . . . . . . 13 |- (z = v -> (z e. A <-> v e. A))
8	7	albidv 1282	. . . . . . . . . . . . 13 |- (z = v -> (A.y z e. A <-> A.y v e. A))
9	7, 8	imbi12d 629	. . . . . . . . . . . 12 |- (z = v -> ((z e. A -> A.y z e. A) <-> (v e. A -> A.y v e. A)))
10	9	a4v 1276	. . . . . . . . . . 11 |- (A.z(z e. A -> A.y z e. A) -> (v e. A -> A.y v e. A))
11	10	adantl 390	. . . . . . . . . 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 988	. . . . . . . . 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 1920	. . . . . . . 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 993	. . . . . . 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 1722	. . . . . . 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 1282	. . . . 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 1830	. . . . 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 536	. . . 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 531	. . 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 1820	. . . . . . 7 |- w e. V
22		sbc6g 1962	. . . . . . . . 9 |- (w e. V -> ([w / x]A.y e. B ph <-> A.x(x = w -> A.y e. B ph)))
23		ralcom4 1830	. . . . . . . . . 10 |- (A.y e. B A.x(x = w -> ph) <-> A.xA.y e. B (x = w -> ph))
24		r19.21v 1723	. . . . . . . . . . 11 |- (A.y e. B (x = w -> ph) <-> (x = w -> A.y e. B ph))
25	24	albii 1003	. . . . . . . . . 10 |- (A.xA.y e. B (x = w -> ph) <-> A.x(x = w -> A.y e. B ph))
26	23, 25	bitr2i 174	. . . . . . . . 9 |- (A.x(x = w -> A.y e. B ph) <-> A.y e. B A.x(x = w -> ph))
27	22, 26	syl6bb 539	. . . . . . . 8 |- (w e. V -> ([w / x]A.y e. B ph <-> A.y e. B A.x(x = w -> ph)))
28		sbc6g 1962	. . . . . . . . 9 |- (w e. V -> ([w / x]ph <-> A.x(x = w -> ph)))
29	28	ralbidv 1670	. . . . . . . 8 |- (w e. V -> (A.y e. B [w / x]ph <-> A.y e. B A.x(x = w -> ph)))
30	27, 29	bitr4d 534	. . . . . . 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 1988	. . . . 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 391	. . . 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 988	. . 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 1962	. . . . . 6 |- (A e. C -> ([A / w][w / x]ph <-> A.w(w = A -> [w / x]ph)))
36	35	adantr 391	. . . . 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 988	. . . 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 1668	. . 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 553	. 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 1959	. . . 4 |- (A e. C -> ([A / w][w / x]A.y e. B ph <-> [A / x]A.y e. B ph))
41	40	adantr 391	. . 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 988	. 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 1959	. . . . 5 |- (A e. C -> ([A / w][w / x]ph <-> [A / x]ph))
44	43	adantr 391	. . . 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 988	. . 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 1668	. 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 551	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 958   = wceq 960   e. wcel 962  [wsbc 1174  A.wral 1652  Vcvv 1818

This theorem is referenced by:  sbcrext 2001  sbcralg 2004

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-9 969  ax-10 970  ax-11 971  ax-12 972  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1127  ax-10o 1144  ax-16 1214  ax-11o 1222  ax-ext 1464

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 985  df-sb 1176  df-clab 1470  df-cleq 1475  df-clel 1478 &nb