Theorem ax10lem2 1937

Description: Lemma for ax10 1944. Change free variable. (Contributed by NM, 25-Jul-2015.)

Assertion

Ref	Expression
ax10lem2	⊢ (∀x x = y → ∀x x = z)

Distinct variable groups:   x,y   x,z

Proof of Theorem ax10lem2

Step	Hyp	Ref	Expression
1		hbe1 1731	. . . 4 ⊢ (∃x ¬ x = y → ∀x∃x ¬ x = y)
2		equequ2 1686	. . . . . . . 8 ⊢ (z = y → (x = z ↔ x = y))
3	2	biimprd 214	. . . . . . 7 ⊢ (z = y → (x = y → x = z))
4	3	con3rr3 128	. . . . . 6 ⊢ (¬ x = z → (z = y → ¬ x = y))
5		19.8a 1756	. . . . . 6 ⊢ (¬ x = y → ∃x ¬ x = y)
6	4, 5	syl6 29	. . . . 5 ⊢ (¬ x = z → (z = y → ∃x ¬ x = y))
7		ax-17 1616	. . . . . 6 ⊢ (¬ z = y → ∀x ¬ z = y)
8		equequ1 1684	. . . . . . . 8 ⊢ (x = z → (x = y ↔ z = y))
9	8	notbid 285	. . . . . . 7 ⊢ (x = z → (¬ x = y ↔ ¬ z = y))
10	9	biimprd 214	. . . . . 6 ⊢ (x = z → (¬ z = y → ¬ x = y))
11	7, 10	spimeh 1667	. . . . 5 ⊢ (¬ z = y → ∃x ¬ x = y)
12	6, 11	pm2.61d1 151	. . . 4 ⊢ (¬ x = z → ∃x ¬ x = y)
13	1, 12	exlimih 1804	. . 3 ⊢ (∃x ¬ x = z → ∃x ¬ x = y)
14		exnal 1574	. . 3 ⊢ (∃x ¬ x = z ↔ ¬ ∀x x = z)
15		exnal 1574	. . 3 ⊢ (∃x ¬ x = y ↔ ¬ ∀x x = y)
16	13, 14, 15	3imtr3i 256	. 2 ⊢ (¬ ∀x x = z → ¬ ∀x x = y)
17	16	con4i 122	1 ⊢ (∀x x = y → ∀x x = z)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4  ∀wal 1540  ∃wex 1541

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746

This proof depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545

This theorem is used by:  ax10lem3  1938