Theorem spw 2033

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206  ∀wal 1535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778

This theorem is referenced by:  hba1w  2047  19.8aw  2050  exexw  2051  spaev  2052  ax12w  2133  rspw  3242  reldisj  4476  ralidmw  4531  dtruALT2  5388  dtruOLD  5461  bj-ssblem1  36620  bj-ax12w  36643  eu6w  42631