Theorem ax12w 2131

Description: Weak version of ax-12 2175 from which we can prove any ax-12 2175 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 2133. (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 2031	. 2 ⊢ (∀𝑦𝜑 → 𝜑)
3		ax12w.1	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	3	ax12wlem 2130	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
5	2, 4	syl5 34	1 ⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777

This theorem is referenced by:  ax12wdemo  2133