Theorem sbequi 1228

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 1227	. . . . . 6 |- (-. A.z z = x -> ([x / z]ph -> A.z[x / z]ph))
2		equvini 1168	. . . . . . . 8 |- (x = y -> E.z(x = z /\ z = y))
3		stdpc7 1180	. . . . . . . . . 10 |- (x = z -> ([x / z]ph -> ph))
4		sbequ1 1178	. . . . . . . . . 10 |- (z = y -> (ph -> [y / z]ph))
5	3, 4	sylan9 468	. . . . . . . . 9 |- ((x = z /\ z = y) -> ([x / z]ph -> [y / z]ph))
6	5	19.22i 1040	. . . . . . . 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 1075	. . . . . . 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 468	. . . . 5 |- ((-. A.z z = x /\ x = y) -> ([x / z]ph -> E.z[y / z]ph))
11		hbnae 1147	. . . . . 6 |- (-. A.z z = y -> A.z -. A.z z = y)
12		hbsb2 1227	. . . . . 6 |- (-. A.z z = y -> ([y / z]ph -> A.z[y / z]ph))
13	11, 12	19.9d 1037	. . . . 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 1179	. . . . . 6 |- (z = x -> ([x / z]ph -> ph))
18	17	a4s 984	. . . . 5 |- (A.z z = x -> ([x / z]ph -> ph))
19	18	adantr 389	. . . 4 |- ((A.z z = x /\ x = y) -> ([x / z]ph -> ph))
20		sbequ1 1178	. . . . 5 |- (x = y -> (ph -> [y / x]ph))
21		drsb1 1175	. . . . . . 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 1143	. . . . 5 |- (A.z z = x -> ([y / x]ph -> [y / z]ph))
24	20, 23	sylan9r 469	. . . 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 1175	. . . . . 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 1180	. . . . 5 |- (x = y -> ([x / y]ph -> ph))
30	28, 29	sylan9 468	. . . 4 |- ((A.z z = y /\ x = y) -> ([x / z]ph -> ph))
31	4	a4s 984	. . . . 5 |- (A.z z = y -> (ph -> [y / z]ph))
32	31	adantr 389	. . . 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 954   = wceq 956  E.wex 980  [wsbc 1170

This theorem is referenced by:  sbequ 1229  drsb2 1230

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-9 965  ax-10 966  ax-12 968  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-11o 1218

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

Copyright terms: Public domain