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

Theorem spw 1701
Description: Weak version of specialization scheme sp 1755. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 1755 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 1755 having no wff metavariables and mutually distinct set variables (see ax11wdemo 1730 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 1755 are spfw 1698 (minimal distinct variable requirements), spnfw 1677 (when  x is not free in  -.  ph), spvw 1673 (when  x does not appear in  ph), sptruw 1678 (when  ph is true), and spfalw 1679 (when  ph is false). (Contributed by NM, 9-Apr-2017.)
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 . . 3  |-  ( A. x ph  ->  A. y A. x ph )
2 ax-5 1563 . . 3  |-  ( A. y ( A. x ph  ->  ps )  -> 
( A. y A. x ph  ->  A. y ps ) )
3 spw.1 . . . . . 6  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
43biimprd 215 . . . . 5  |-  ( x  =  y  ->  ( ps  ->  ph ) )
54equcoms 1688 . . . 4  |-  ( y  =  x  ->  ( ps  ->  ph ) )
65spimvw 1676 . . 3  |-  ( A. y ps  ->  ph )
71, 2, 6syl56 32 . 2  |-  ( A. y ( A. x ph  ->  ps )  -> 
( A. x ph  ->  ph ) )
83biimpd 199 . . 3  |-  ( x  =  y  ->  ( ph  ->  ps ) )
98spimvw 1676 . 2  |-  ( A. x ph  ->  ps )
107, 9mpg 1554 1  |-  ( A. x ph  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1546
This theorem is referenced by:  spvwOLD  1702  spfalwOLD  1706  hba1w  1714  ax11w  1728
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 1661  ax-8 1682
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548
  Copyright terms: Public domain W3C validator