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

Theorem spw 1679
Description: Weak version of specialization scheme sp 1728. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 1728 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 1728 having no wff metavariables and mutually distinct set variables (see ax11wdemo 1709 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 1728 are spfw 1676 (minimal distinct variable requirements), spnfw 1658 (when  x is not free in  -.  ph), spvw 1655 (when  x does not appear in  ph), sptruw 1684 (when  ph is true), and spfalw 1685 (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 1606 . . 3  |-  ( A. x ph  ->  A. y A. x ph )
2 ax-5 1547 . . 3  |-  ( A. y ( A. x ph  ->  ps )  -> 
( A. y A. x ph  ->  A. y ps ) )
3 spw.1 . . . . . 6  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
43biimprd 214 . . . . 5  |-  ( x  =  y  ->  ( ps  ->  ph ) )
54equcoms 1666 . . . 4  |-  ( y  =  x  ->  ( ps  ->  ph ) )
65spimvw 1657 . . 3  |-  ( A. y ps  ->  ph )
71, 2, 6syl56 30 . 2  |-  ( A. y ( A. x ph  ->  ps )  -> 
( A. x ph  ->  ph ) )
83biimpd 198 . . 3  |-  ( x  =  y  ->  ( ph  ->  ps ) )
98spimvw 1657 . 2  |-  ( A. x ph  ->  ps )
107, 9mpg 1538 1  |-  ( A. x ph  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1530
This theorem is referenced by:  spvwOLD  1680  spfalw  1685  hba1w  1693  ax11w  1707
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532
  Copyright terms: Public domain W3C validator