Theorem sbequi 1598

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 1597	. . . . . 6 |- (-. A.z z = x -> ([x / z]ph -> A.z[x / z]ph))
2		equvini 1531	. . . . . . . 8 |- (x = y -> E.z(x = z /\ z = y))
3		stdpc7 1544	. . . . . . . . . 10 |- (x = z -> ([x / z]ph -> ph))
4		sbequ1 1542	. . . . . . . . . 10 |- (z = y -> (ph -> [y / z]ph))
5	3, 4	sylan9 517	. . . . . . . . 9 |- ((x = z /\ z = y) -> ([x / z]ph -> [y / z]ph))
6	5	eximi 1387	. . . . . . . 8 |- (E.z(x = z /\ z = y) -> E.z([x / z]ph -> [y / z]ph))
7	2, 6	syl 12	. . . . . . 7 |- (x = y -> E.z([x / z]ph -> [y / z]ph))
8		19.35 1426	. . . . . . 7 |- (E.z([x / z]ph -> [y / z]ph) <-> (A.z[x / z]ph -> E.z[y / z]ph))
9	7, 8	sylib 215	. . . . . 6 |- (x = y -> (A.z[x / z]ph -> E.z[y / z]ph))
10	1, 9	sylan9 517	. . . . 5 |- ((-. A.z z = x /\ x = y) -> ([x / z]ph -> E.z[y / z]ph))
11		hbnae 1507	. . . . . 6 |- (-. A.z z = y -> A.z -. A.z z = y)
12		hbsb2 1597	. . . . . 6 |- (-. A.z z = y -> ([y / z]ph -> A.z[y / z]ph))
13	11, 12	19.9d 1384	. . . . 5 |- (-. A.z z = y -> (E.z[y / z]ph -> [y / z]ph))
14	10, 13	syl9 71	. . . 4 |- ((-. A.z z = x /\ x = y) -> (-. A.z z = y -> ([x / z]ph -> [y / z]ph)))
15	14	ex 402	. . 3 |- (-. A.z z = x -> (x = y -> (-. A.z z = y -> ([x / z]ph -> [y / z]ph))))
16	15	com23 36	. 2 |- (-. A.z z = x -> (-. A.z z = y -> (x = y -> ([x / z]ph -> [y / z]ph))))
17		sbequ2 1543	. . . . . 6 |- (z = x -> ([x / z]ph -> ph))
18	17	a4s 1330	. . . . 5 |- (A.z z = x -> ([x / z]ph -> ph))
19	18	adantr 425	. . . 4 |- ((A.z z = x /\ x = y) -> ([x / z]ph -> ph))
20		sbequ1 1542	. . . . 5 |- (x = y -> (ph -> [y / x]ph))
21		drsb1 1539	. . . . . . 7 |- (A.x x = z -> ([y / x]ph <-> [y / z]ph))
22	21	biimpd 170	. . . . . 6 |- (A.x x = z -> ([y / x]ph -> [y / z]ph))
23	22	alequcoms 1503	. . . . 5 |- (A.z z = x -> ([y / x]ph -> [y / z]ph))
24	20, 23	sylan9r 519	. . . 4 |- ((A.z z = x /\ x = y) -> (ph -> [y / z]ph))
25	19, 24	syld 30	. . 3 |- ((A.z z = x /\ x = y) -> ([x / z]ph -> [y / z]ph))
26	25	ex 402	. 2 |- (A.z z = x -> (x = y -> ([x / z]ph -> [y / z]ph)))
27		drsb1 1539	. . . . . 6 |- (A.z z = y -> ([x / z]ph <-> [x / y]ph))
28	27	biimpd 170	. . . . 5 |- (A.z z = y -> ([x / z]ph -> [x / y]ph))
29		stdpc7 1544	. . . . 5 |- (x = y -> ([x / y]ph -> ph))
30	28, 29	sylan9 517	. . . 4 |- ((A.z z = y /\ x = y) -> ([x / z]ph -> ph))
31	4	a4s 1330	. . . . 5 |- (A.z z = y -> (ph -> [y / z]ph))
32	31	adantr 425	. . . 4 |- ((A.z z = y /\ x = y) -> (ph -> [y / z]ph))
33	30, 32	syld 30	. . 3 |- ((A.z z = y /\ x = y) -> ([x / z]ph -> [y / z]ph))
34	33	ex 402	. 2 |- (A.z z = y -> (x = y -> ([x / z]ph -> [y / z]ph)))
35	16, 26, 34	pm2.61ii 144	1 |- (x = y -> ([x / z]ph -> [y / z]ph))

Syntax hints:  -. wn 2   -> wi 3   /\ wa 240  A.wal 1296   = wceq 1298  E.wex 1326  [wsbc 1534

This theorem is referenced by:  sbequ 1599

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-12 1310  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-11o 1588

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536

Copyright terms: Public domain