Theorem sbcralt 1986

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 1951	. . . . . 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 982	. . . 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 1001	. . . . . . . . 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 969	. . . . . . . . . 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 1531	. . . . . . . . . . . . 13 |- (z = v -> (z e. A <-> v e. A))
8	7	albidv 1276	. . . . . . . . . . . . 13 |- (z = v -> (A.y z e. A <-> A.y v e. A))
9	7, 8	imbi12d 625	. . . . . . . . . . . 12 |- (z = v -> ((z e. A -> A.y z e. A) <-> (v e. A -> A.y v e. A)))
10	9	a4v 1270	. . . . . . . . . . 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 982	. . . . . . . . 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 1909	. . . . . . . 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 987	. . . . . . 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 1712	. . . . . . 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 1276	. . . . 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 1819	. . . . 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 532	. . . 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 527	. . 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 1809	. . . . . . 7 |- w e. V
22		sbc6g 1951	. . . . . . . . 9 |- (w e. V -> ([w / x]A.y e. B ph <-> A.x(x = w -> A.y e. B ph)))
23		ralcom4 1819	. . . . . . . . . 10 |- (A.y e. B A.x(x = w -> ph) <-> A.xA.y e. B (x = w -> ph))
24		r19.21v 1713	. . . . . . . . . . 11 |- (A.y e. B (x = w -> ph) <-> (x = w -> A.y e. B ph))
25	24	albii 997	. . . . . . . . . 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 535	. . . . . . . 8 |- (w e. V -> ([w / x]A.y e. B ph <-> A.y e. B A.x(x = w -> ph)))
28		sbc6g 1951	. . . . . . . . 9 |- (w e. V -> ([w / x]ph <-> A.x(x = w -> ph)))
29	28	ralbidv 1660	. . . . . . . 8 |- (w e. V -> (A.y e. B [w / x]ph <-> A.y e. B A.x(x = w -> ph)))
30	27, 29	bitr4d 530	. . . . . . 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 1974	. . . . 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 982	. . 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 1951	. . . . . 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 982	. . . 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 1658	. . 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 549	. 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 1948	. . . 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 982	. 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 1948	. . . . 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 982	. . 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 1658	. 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 547	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 952   = wceq 954   e. wcel 956  [wsbc 1168  A.wral 1642  Vcvv 1807

This theorem is referenced by:  sbcrext 1987  sbcralg 1990

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470