Theorem spw 2067

Description: Weak version of the specialization scheme sp 2222. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 2222 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 2222 having mutually distinct setvar variables and no wff metavariables (see ax12wdemo 2173 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 2222 are spfw 2066 (minimal distinct variable requirements), spnfw 2012 (when 𝑥 is not free in ¬ 𝜑), spvw 2014 (when 𝑥 does not appear in 𝜑), sptruw 1839 (when 𝜑 is true), spfalw 2013 (when 𝜑 is false), and spvv 2021 (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 1943	. 2 ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓)
2		ax-5 1943	. 2 ⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑)
3		ax-5 1943	. 2 ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑)
4		spw.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
5	1, 2, 3, 4	spfw 2066	1 ⊢ (∀𝑥𝜑 → 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

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

This theorem is used by:  hba1w  2082  19.8aw  2085  exexw  2086  spaev  2087  ax12w  2171  rspw  3244  reldisj  4413  ralidmw  4479  dtruALT2  5343  bj-ssblem1  37335  bj-ax12w  37359  eu6w  43468