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

Theorem spw 1861
Description: Weak version of the specialization scheme sp 1914. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 1914 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 1914 having mutually distinct setvar variables and no wff metavariables (see ax12wdemo 1885 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 1914 are spfw 1860 (minimal distinct variable requirements), spnfw 1837 (when  x is not free in  -.  ph), spvw 1807 (when  x does not appear in  ph), sptruw 1675 (when  ph is true), and spfalw 1838 (when  ph is false). (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 27-Feb-2018.)
Hypothesis
Ref Expression
spw.1  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
spw  |-  ( A. x ph  ->  ph )
Distinct variable groups:    x, y    ps, x    ph, y
Allowed substitution hints:    ph( x)    ps( y)

Proof of Theorem spw
StepHypRef Expression
1 ax-5 1752 . 2  |-  ( -. 
ps  ->  A. x  -.  ps )
2 ax-5 1752 . 2  |-  ( A. x ph  ->  A. y A. x ph )
3 ax-5 1752 . 2  |-  ( -. 
ph  ->  A. y  -.  ph )
4 spw.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
51, 2, 3, 4spfw 1860 1  |-  ( A. x ph  ->  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187   A.wal 1435
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843
This theorem depends on definitions:  df-bi 188  df-ex 1658
This theorem is referenced by:  hba1w  1868  ax12w  1883  bj-ax12w  31236
  Copyright terms: Public domain W3C validator