Theorem sbequi 876

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 873	. . . . . 6 |- (-. A.z z = x -> ([x / z]ph -> A.z[x / z]ph))
2		eqvin.l1 851	. . . . . . . 8 |- (x = y -> E.z(x = z /\ z = y))
3		sbequ2 864	. . . . . . . . . . 11 |- (z = x -> ([x / z]ph -> ph))
4	3	eqcoms 813	. . . . . . . . . 10 |- (x = z -> ([x / z]ph -> ph))
5		sbequ1 863	. . . . . . . . . 10 |- (z = y -> (ph -> [y / z]ph))
6	4, 5	sylan9 359	. . . . . . . . 9 |- ((x = z /\ z = y) -> ([x / z]ph -> [y / z]ph))
7	6	19.22i 723	. . . . . . . 8 |- (E.z(x = z /\ z = y) -> E.z([x / z]ph -> [y / z]ph))
8	2, 7	syl 12	. . . . . . 7 |- (x = y -> E.z([x / z]ph -> [y / z]ph))
9		19.35 754	. . . . . . 7 |- (E.z([x / z]ph -> [y / z]ph) <-> (A.z[x / z]ph -> E.z[y / z]ph))
10	8, 9	sylib 173	. . . . . 6 |- (x = y -> (A.z[x / z]ph -> E.z[y / z]ph))
11	1, 10	sylan9 359	. . . . 5 |- ((-. A.z z = x /\ x = y) -> ([x / z]ph -> E.z[y / z]ph))
12		eq6 826	. . . . . 6 |- (-. A.z z = y -> A.z -. A.z z = y)
13		hbsb2 873	. . . . . 6 |- (-. A.z z = y -> ([y / z]ph -> A.z[y / z]ph))
14	12, 13	19.9d 720	. . . . 5 |- (-. A.z z = y -> (E.z[y / z]ph -> [y / z]ph))
15	11, 14	syl9 55	. . . 4 |- ((-. A.z z = x /\ x = y) -> (-. A.z z = y -> ([x / z]ph -> [y / z]ph)))
16	15	exp 291	. . 3 |- (-. A.z z = x -> (x = y -> (-. A.z z = y -> ([x / z]ph -> [y / z]ph))))
17	16	com23 32	. 2 |- (-. A.z z = x -> (-. A.z z = y -> (x = y -> ([x / z]ph -> [y / z]ph))))
18	3	a4s 682	. . . . 5 |- (A.z z = x -> ([x / z]ph -> ph))
19	18	adantr 306	. . . 4 |- ((A.z z = x /\ x = y) -> ([x / z]ph -> ph))
20		sbequ1 863	. . . . 5 |- (x = y -> (ph -> [y / x]ph))
21		del43 856	. . . . . 6 |- (A.x x = z -> ([y / x]ph -> [y / z]ph))
22	21	eq4s 822	. . . . 5 |- (A.z z = x -> ([y / x]ph -> [y / z]ph))
23	20, 22	sylan9r 360	. . . 4 |- ((A.z z = x /\ x = y) -> (ph -> [y / z]ph))
24	19, 23	syld 27	. . 3 |- ((A.z z = x /\ x = y) -> ([x / z]ph -> [y / z]ph))
25	24	exp 291	. 2 |- (A.z z = x -> (x = y -> ([x / z]ph -> [y / z]ph)))
26		del43 856	. . . . 5 |- (A.z z = y -> ([x / z]ph -> [x / y]ph))
27		sbequ2 864	. . . . . 6 |- (y = x -> ([x / y]ph -> ph))
28	27	eqcoms 813	. . . . 5 |- (x = y -> ([x / y]ph -> ph))
29	26, 28	sylan9 359	. . . 4 |- ((A.z z = y /\ x = y) -> ([x / z]ph -> ph))
30	5	a4s 682	. . . . 5 |- (A.z z = y -> (ph -> [y / z]ph))
31	30	adantr 306	. . . 4 |- ((A.z z = y /\ x = y) -> (ph -> [y / z]ph))
32	29, 31	syld 27	. . 3 |- ((A.z z = y /\ x = y) -> ([x / z]ph -> [y / z]ph))
33	32	exp 291	. 2 |- (A.z z = y -> (x = y -> ([x / z]ph -> [y / z]ph)))
34	17, 25, 33	pm2.61ii 113	1 |- (x = y -> ([x / z]ph -> [y / z]ph))

Syntax hints:  -. wn 1   -> wi 2   /\ wa 196  A.wal 672  E.wex 678   = weq 797  [wsb 852

This theorem is referenced by:  sbequ 877  del44 878  del45 879

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853

metamath.org