Theorem sbequi 876

Description: An equality theorem for substitution.

Assertion

Ref	Expression
sbequi	⊢ (x = y → ([x / z]φ → [y / z]φ))

Proof of Theorem sbequi

Step	Hyp	Ref	Expression
1		hbsb2 873	. . . . . 6 ⊢ (¬ ∀z z = x → ([x / z]φ → ∀z[x / z]φ))
2		eqvin.l1 851	. . . . . . . 8 ⊢ (x = y → ∃z(x = z ∧ z = y))
3		sbequ2 864	. . . . . . . . . . 11 ⊢ (z = x → ([x / z]φ → φ))
4	3	eqcoms 813	. . . . . . . . . 10 ⊢ (x = z → ([x / z]φ → φ))
5		sbequ1 863	. . . . . . . . . 10 ⊢ (z = y → (φ → [y / z]φ))
6	4, 5	sylan9 359	. . . . . . . . 9 ⊢ ((x = z ∧ z = y) → ([x / z]φ → [y / z]φ))
7	6	19.22i 723	. . . . . . . 8 ⊢ (∃z(x = z ∧ z = y) → ∃z([x / z]φ → [y / z]φ))
8	2, 7	syl 12	. . . . . . 7 ⊢ (x = y → ∃z([x / z]φ → [y / z]φ))
9		19.35 754	. . . . . . 7 ⊢ (∃z([x / z]φ → [y / z]φ) ↔ (∀z[x / z]φ → ∃z[y / z]φ))
10	8, 9	sylib 173	. . . . . 6 ⊢ (x = y → (∀z[x / z]φ → ∃z[y / z]φ))
11	1, 10	sylan9 359	. . . . 5 ⊢ ((¬ ∀z z = x ∧ x = y) → ([x / z]φ → ∃z[y / z]φ))
12		eq6 826	. . . . . 6 ⊢ (¬ ∀z z = y → ∀z ¬ ∀z z = y)
13		hbsb2 873	. . . . . 6 ⊢ (¬ ∀z z = y → ([y / z]φ → ∀z[y / z]φ))
14	12, 13	19.9d 720	. . . . 5 ⊢ (¬ ∀z z = y → (∃z[y / z]φ → [y / z]φ))
15	11, 14	syl9 55	. . . 4 ⊢ ((¬ ∀z z = x ∧ x = y) → (¬ ∀z z = y → ([x / z]φ → [y / z]φ)))
16	15	exp 291	. . 3 ⊢ (¬ ∀z z = x → (x = y → (¬ ∀z z = y → ([x / z]φ → [y / z]φ))))
17	16	com23 32	. 2 ⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x = y → ([x / z]φ → [y / z]φ))))
18	3	a4s 682	. . . . 5 ⊢ (∀z z = x → ([x / z]φ → φ))
19	18	adantr 306	. . . 4 ⊢ ((∀z z = x ∧ x = y) → ([x / z]φ → φ))
20		sbequ1 863	. . . . 5 ⊢ (x = y → (φ → [y / x]φ))
21		del43 856	. . . . . 6 ⊢ (∀x x = z → ([y / x]φ → [y / z]φ))
22	21	eq4s 822	. . . . 5 ⊢ (∀z z = x → ([y / x]φ → [y / z]φ))
23	20, 22	sylan9r 360	. . . 4 ⊢ ((∀z z = x ∧ x = y) → (φ → [y / z]φ))
24	19, 23	syld 27	. . 3 ⊢ ((∀z z = x ∧ x = y) → ([x / z]φ → [y / z]φ))
25	24	exp 291	. 2 ⊢ (∀z z = x → (x = y → ([x / z]φ → [y / z]φ)))
26		del43 856	. . . . 5 ⊢ (∀z z = y → ([x / z]φ → [x / y]φ))
27		sbequ2 864	. . . . . 6 ⊢ (y = x → ([x / y]φ → φ))
28	27	eqcoms 813	. . . . 5 ⊢ (x = y → ([x / y]φ → φ))
29	26, 28	sylan9 359	. . . 4 ⊢ ((∀z z = y ∧ x = y) → ([x / z]φ → φ))
30	5	a4s 682	. . . . 5 ⊢ (∀z z = y → (φ → [y / z]φ))
31	30	adantr 306	. . . 4 ⊢ ((∀z z = y ∧ x = y) → (φ → [y / z]φ))
32	29, 31	syld 27	. . 3 ⊢ ((∀z z = y ∧ x = y) → ([x / z]φ → [y / z]φ))
33	32	exp 291	. 2 ⊢ (∀z z = y → (x = y → ([x / z]φ → [y / z]φ)))
34	17, 25, 33	pm2.61ii 113	1 ⊢ (x = y → ([x / z]φ → [y / z]φ))

Syntax hints:  ¬ wn 1   → wi 2   ∧ wa 196  ∀wal 672  ∃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