Theorem spw 2067

Description: Weak version of the specialization scheme sp 2220. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 2220 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 2220 having mutually distinct setvar variables and no wff metavariables (see ax12wdemo 2172 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 2220 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  2170  rspw  3240  reldisj  4406  ralidmw  4472  dtruALT2  5332  bj-ssblem1  37553  bj-ax12w  37577  eu6w  43687