Theorem spw 2041

Description: Weak version of the specialization scheme sp 2180. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 2180 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 2180 having mutually distinct setvar variables and no wff metavariables (see ax12wdemo 2135 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 2180 are spfw 2040 (minimal distinct variable requirements), spnfw 1987 (when 𝑥 is not free in ¬ 𝜑), spvw 1988 (when 𝑥 does not appear in 𝜑), sptruw 1813 (when 𝜑 is true), spfalw 2005 (when 𝜑 is false), and spvv 2004 (where 𝜑 is changed into 𝜓). (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 27-Feb-2018.)

Hypothesis

Ref	Expression
spw.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
spw	⊢ (∀𝑥𝜑 → 𝜑)

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

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem spw

Step	Hyp	Ref	Expression
1		ax-5 1917	. 2 ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓)
2		ax-5 1917	. 2 ⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑)
3		ax-5 1917	. 2 ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑)
4		spw.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
5	1, 2, 3, 4	spfw 2040	1 ⊢ (∀𝑥𝜑 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787

This theorem is referenced by:  hba1w  2054  19.8aw  2057  exexw  2058  spaev  2059  ax12w  2133  nfcriOLD  2899  rspw  3131  reldisj  4391  ralidmw  4444  dtru  5297  bj-ssblem1  34823  bj-ax12w  34846