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

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