Theorem spw 2068

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 2067 (minimal distinct variable requirements), spnfw 2013 (when 𝑥 is not free in ¬ 𝜑), spvw 2015 (when 𝑥 does not appear in 𝜑), sptruw 1838 (when 𝜑 is true), spfalw 2014 (when 𝜑 is false), and spvv 2022 (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 1944	. 2 ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓)
2		ax-5 1944	. 2 ⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑)
3		ax-5 1944	. 2 ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑)
4		spw.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
5	1, 2, 3, 4	spfw 2067	1 ⊢ (∀𝑥𝜑 → 𝜑)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042

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

This theorem is used by:  hba1w  2083  19.8aw  2086  exexw  2087  spaev  2088  ax12w  2171  rspw  3242  reldisj  4408  ralidmw  4474  dtruALT2  5335  bj-ssblem1  37680  bj-ax12w  37704  eu6w  43827