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

Theorem spw 2123
Description: Weak version of the specialization scheme sp 2207. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 2207 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 2207 having mutually distinct setvar variables and no wff metavariables (see ax12wdemo 2167 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 2207 are spfw 2121 (minimal distinct variable requirements), spnfw 2086 (when 𝑥 is not free in ¬ 𝜑), spvw 2067 (when 𝑥 does not appear in 𝜑), sptruw 1881 (when 𝜑 is true), and spfalw 2087 (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 1991 . 2 𝜓 → ∀𝑥 ¬ 𝜓)
2 ax-5 1991 . 2 (∀𝑥𝜑 → ∀𝑦𝑥𝜑)
3 ax-5 1991 . 2 𝜑 → ∀𝑦 ¬ 𝜑)
4 spw.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
51, 2, 3, 4spfw 2121 1 (∀𝑥𝜑𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wal 1629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853
This theorem is referenced by:  hba1w  2131  hba1wOLD  2132  spaev  2135  ax12w  2165  bj-ssblem1  32968  bj-ax12w  33002
  Copyright terms: Public domain W3C validator