Theorem a16g 1945

Description: Generalization of ax16 2045. (Contributed by NM, 25-Jul-2015.)

Assertion

Ref	Expression
a16g	⊢ (∀x x = y → (φ → ∀zφ))

Distinct variable group:   x,y

Allowed substitution hints:   φ(x, y, z)

Proof of Theorem a16g

Dummy variable w is distinct from all other variables.

Step	Hyp	Ref	Expression
1		a9ev 1656	. 2 ⊢ ∃w w = z
2		ax10lem5 1942	. 2 ⊢ (∀x x = y → ∀w w = z)
3		hbn1 1730	. . . . 5 ⊢ (¬ ∀w w = z → ∀w ¬ ∀w w = z)
4		pm2.21 100	. . . . 5 ⊢ (¬ ∀w w = z → (∀w w = z → (φ → ∀zφ)))
5	3, 4	alrimih 1565	. . . 4 ⊢ (¬ ∀w w = z → ∀w(∀w w = z → (φ → ∀zφ)))
6		ax-17 1616	. . . . 5 ⊢ ((φ → ∀zφ) → ∀w(φ → ∀zφ))
7		ax-1 6	. . . . 5 ⊢ ((φ → ∀zφ) → (∀w w = z → (φ → ∀zφ)))
8	6, 7	alrimih 1565	. . . 4 ⊢ ((φ → ∀zφ) → ∀w(∀w w = z → (φ → ∀zφ)))
9	5, 8	ja 153	. . 3 ⊢ ((∀w w = z → (φ → ∀zφ)) → ∀w(∀w w = z → (φ → ∀zφ)))
10		ax10lem5 1942	. . . 4 ⊢ (∀w w = z → ∀z z = w)
11		equcomi 1679	. . . . . . 7 ⊢ (w = z → z = w)
12		ax-17 1616	. . . . . . 7 ⊢ (φ → ∀wφ)
13		ax-11 1746	. . . . . . 7 ⊢ (z = w → (∀wφ → ∀z(z = w → φ)))
14	11, 12, 13	syl2im 34	. . . . . 6 ⊢ (w = z → (φ → ∀z(z = w → φ)))
15		ax-5 1557	. . . . . 6 ⊢ (∀z(z = w → φ) → (∀z z = w → ∀zφ))
16	14, 15	syl6 29	. . . . 5 ⊢ (w = z → (φ → (∀z z = w → ∀zφ)))
17	16	com23 72	. . . 4 ⊢ (w = z → (∀z z = w → (φ → ∀zφ)))
18	10, 17	syl5 28	. . 3 ⊢ (w = z → (∀w w = z → (φ → ∀zφ)))
19	9, 18	exlimih 1804	. 2 ⊢ (∃w w = z → (∀w w = z → (φ → ∀zφ)))
20	1, 2, 19	mpsyl 59	1 ⊢ (∀x x = y → (φ → ∀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-7 1734  ax-11 1746  ax-12 1925

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

This theorem is used by:  ax16  2045  a16gb  2050  a16nf  2051