MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  spw Structured version   Visualization version   GIF version

Theorem spw 2032
Description: Weak version of the specialization scheme sp 2172. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 2172 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 2172 having mutually distinct setvar variables and no wff metavariables (see ax12wdemo 2130 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 2172 are spfw 2031 (minimal distinct variable requirements), spnfw 1975 (when 𝑥 is not free in ¬ 𝜑), spvw 1976 (when 𝑥 does not appear in 𝜑), sptruw 1798 (when 𝜑 is true), and spfalw 1995 (when 𝜑 is false). (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
StepHypRef Expression
1 ax-5 1902 . 2 𝜓 → ∀𝑥 ¬ 𝜓)
2 ax-5 1902 . 2 (∀𝑥𝜑 → ∀𝑦𝑥𝜑)
3 ax-5 1902 . 2 𝜑 → ∀𝑦 ¬ 𝜑)
4 spw.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
51, 2, 3, 4spfw 2031 1 (∀𝑥𝜑𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wal 1526
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772
This theorem is referenced by:  hba1w  2045  spaev  2048  ax12w  2128  bj-ssblem1  33884  bj-ax12w  33907
  Copyright terms: Public domain W3C validator