Theorem sbequi 1230

Description: An equality theorem for substitution.

Assertion

Ref	Expression
sbequi	|- (x = y -> ([x / z]ph -> [y / z]ph))

Proof of Theorem sbequi

Step	Hyp	Ref	Expression
1		hbsb2 1229	. . . . . 6 |- (-. A.z z = x -> ([x / z]ph -> A.z[x / z]ph))
2		equvini 1170	. . . . . . . 8 |- (x = y -> E.z(x = z /\ z = y))
3		stdpc7 1182	. . . . . . . . . 10 |- (x = z -> ([x / z]ph -> ph))
4		sbequ1 1180	. . . . . . . . . 10 |- (z = y -> (ph -> [y / z]ph))
5	3, 4	sylan9 470	. . . . . . . . 9 |- ((x = z /\ z = y) -> ([x / z]ph -> [y / z]ph))
6	5	19.22i 1042	. . . . . . . 8 |- (E.z(x = z /\ z = y) -> E.z([x / z]ph -> [y / z]ph))
7	2, 6	syl 10	. . . . . . 7 |- (x = y -> E.z([x / z]ph -> [y / z]ph))
8		19.35 1077	. . . . . . 7 |- (E.z([x / z]ph -> [y / z]ph) <-> (A.z[x / z]ph -> E.z[y / z]ph))
9	7, 8	sylib 198	. . . . . 6 |- (x = y -> (A.z[x / z]ph -> E.z[y / z]ph))
10	1, 9	sylan9 470	. . . . 5 |- ((-. A.z z = x /\ x = y) -> ([x / z]ph -> E.z[y / z]ph))
11		hbnae 1149	. . . . . 6 |- (-. A.z z = y -> A.z -. A.z z = y)
12		hbsb2 1229	. . . . . 6 |- (-. A.z z = y -> ([y / z]ph -> A.z[y / z]ph))
13	11, 12	19.9d 1039	. . . . 5 |- (-. A.z z = y -> (E.z[y / z]ph -> [y / z]ph))
14	10, 13	syl9 57	. . . 4 |- ((-. A.z z = x /\ x = y) -> (-. A.z z = y -> ([x / z]ph -> [y / z]ph)))
15	14	ex 373	. . 3 |- (-. A.z z = x -> (x = y -> (-. A.z z = y -> ([x / z]ph -> [y / z]ph))))
16	15	com23 32	. 2 |- (-. A.z z = x -> (-. A.z z = y -> (x = y -> ([x / z]ph -> [y / z]ph))))
17		sbequ2 1181	. . . . . 6 |- (z = x -> ([x / z]ph -> ph))
18	17	a4s 986	. . . . 5 |- (A.z z = x -> ([x / z]ph -> ph))
19	18	adantr 391	. . . 4 |- ((A.z z = x /\ x = y) -> ([x / z]ph -> ph))
20		sbequ1 1180	. . . . 5 |- (x = y -> (ph -> [y / x]ph))
21		drsb1 1177	. . . . . . 7 |- (A.x x = z -> ([y / x]ph <-> [y / z]ph))
22	21	biimpd 153	. . . . . 6 |- (A.x x = z -> ([y / x]ph -> [y / z]ph))
23	22	alequcoms 1145	. . . . 5 |- (A.z z = x -> ([y / x]ph -> [y / z]ph))
24	20, 23	sylan9r 471	. . . 4 |- ((A.z z = x /\ x = y) -> (ph -> [y / z]ph))
25	19, 24	syld 27	. . 3 |- ((A.z z = x /\ x = y) -> ([x / z]ph -> [y / z]ph))
26	25	ex 373	. 2 |- (A.z z = x -> (x = y -> ([x / z]ph -> [y / z]ph)))
27		drsb1 1177	. . . . . 6 |- (A.z z = y -> ([x / z]ph <-> [x / y]ph))
28	27	biimpd 153	. . . . 5 |- (A.z z = y -> ([x / z]ph -> [x / y]ph))
29		stdpc7 1182	. . . . 5 |- (x = y -> ([x / y]ph -> ph))
30	28, 29	sylan9 470	. . . 4 |- ((A.z z = y /\ x = y) -> ([x / z]ph -> ph))
31	4	a4s 986	. . . . 5 |- (A.z z = y -> (ph -> [y / z]ph))
32	31	adantr 391	. . . 4 |- ((A.z z = y /\ x = y) -> (ph -> [y / z]ph))
33	30, 32	syld 27	. . 3 |- ((A.z z = y /\ x = y) -> ([x / z]ph -> [y / z]ph))
34	33	ex 373	. 2 |- (A.z z = y -> (x = y -> ([x / z]ph -> [y / z]ph)))
35	16, 26, 34	pm2.61ii 130	1 |- (x = y -> ([x / z]ph -> [y / z]ph))

Syntax hints:  -. wn 2   -> wi 3   /\ wa 223  A.wal 956   = wceq 958  E.wex 982  [wsbc 1172

This theorem is referenced by:  sbequ 1231  drsb2 1232

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-12 970  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-11o 1220

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174

Copyright terms: Public domain