Theorem ax12w 2171

Description: Weak version of ax-12 2215 from which we can prove any ax-12 2215 instance not involving wff variables or bundling. Uses only Tarski's FOL axiom schemes. An instance of the first hypothesis will normally require that 𝑥 and 𝑦 be distinct (unless 𝑥 does not occur in 𝜑). For an example of how the hypotheses can be eliminated when we substitute an expression without wff variables for 𝜑, see ax12wdemo 2173. (Contributed by NM, 10-Apr-2017.)

Hypotheses

Ref	Expression
ax12w.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
ax12w.2	⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜒))

Assertion

Ref	Expression
ax12w	⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))

Distinct variable groups:   𝑦,𝑧   𝜓,𝑥   𝜑,𝑧   𝜒,𝑦

Allowed substitution hints:   𝜑(𝑥, 𝑦)   𝜓(𝑦, 𝑧)   𝜒(𝑥, 𝑧)

Proof of Theorem ax12w

Step	Hyp	Ref	Expression
1		ax12w.2	. . 3 ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜒))
2	1	spw 2068	. 2 ⊢ (∀𝑦𝜑 → 𝜑)
3		ax12w.1	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	3	ax12wlem 2170	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
5	2, 4	syl5 35	1 ⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1567

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812

This theorem is used by:  ax12wdemo  2173