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

Theorem spw 1706
Description: Weak version of specialization scheme sp 1763. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 1763 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 1763 having no wff metavariables and mutually distinct set variables (see ax11wdemo 1738 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 1763 are spfw 1703 (minimal distinct variable requirements), spnfw 1682 (when  x is not free in  -.  ph), spvw 1678 (when  x does not appear in  ph), sptruw 1683 (when  ph is true), and spfalw 1684 (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-17 1626 . 2  |-  ( -. 
ps  ->  A. x  -.  ps )
2 ax-17 1626 . 2  |-  ( A. x ph  ->  A. y A. x ph )
3 ax-17 1626 . 2  |-  ( -. 
ph  ->  A. y  -.  ph )
4 spw.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
51, 2, 3, 4spfw 1703 1  |-  ( A. x ph  ->  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177   A.wal 1549
This theorem is referenced by:  spvwOLD  1708  spfalwOLD  1712  hba1w  1722  ax11w  1736
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551
  Copyright terms: Public domain W3C validator