Theorem spw 2069

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

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

This theorem is used by:  hba1w  2084  19.8aw  2087  exexw  2088  spaev  2089  ax12w  2172  rspw  3243  reldisj  4409  ralidmw  4475  dtruALT2  5339  bj-ssblem1  37768  bj-ax12w  37792  eu6w  43953