Theorem spw 2041

Description: Weak version of the specialization scheme sp 2195. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 2195 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 2195 having mutually distinct setvar variables and no wff metavariables (see ax12wdemo 2146 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 2195 are spfw 2040 (minimal distinct variable requirements), spnfw 1986 (when 𝑥 is not free in ¬ 𝜑), spvw 1988 (when 𝑥 does not appear in 𝜑), sptruw 1813 (when 𝜑 is true), spfalw 1987 (when 𝜑 is false), and spvv 1995 (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 207  ∀wal 1545

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 1974  ax-7 2015

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

This theorem is referenced by:  hba1w  2056  19.8aw  2059  exexw  2060  spaev  2061  ax12w  2144  rspw  3216  reldisj  4381  ralidmw  4444  dtruALT2  5299  bj-ssblem1  36994  bj-ax12w  37018  eu6w  43126