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

Theorem sp 1716
Description: Specialization. A universally quantified wff implies the wff without a quantifier Axiom scheme B5 of [Tarski] p. 67 (under his system S2, defined in the last paragraph on p. 77). Also appears as Axiom scheme C5' in [Megill] p. 448 (p. 16 of the preprint).

For the axiom of specialization presented in many logic textbooks, see theorem stdpc4 1964.

This theorem shows that our obsolete axiom ax-4 2074 can be derived from the others. The proof uses ideas from the proof of Lemma 21 of [Monk2] p. 114.

It appears that this scheme cannot be derived directly from Tarski's axioms without auxilliary axiom scheme ax-11 1715. It is thought the best we can do using only Tarski's axioms is spw 1660. (Contributed by NM, 21-May-2008.) (Proof shortened by Scott Fenton, 24-Jan-2011.)

Assertion
Ref Expression
sp  |-  ( A. x ph  ->  ph )

Proof of Theorem sp
Dummy variable  w is distinct from all other variables.
StepHypRef Expression
1 ax9v 1636 . 2  |-  -.  A. w  -.  w  =  x
2 equcomi 1646 . . . . . . 7  |-  ( w  =  x  ->  x  =  w )
3 ax-17 1603 . . . . . . 7  |-  ( -. 
ph  ->  A. w  -.  ph )
4 ax-11 1715 . . . . . . 7  |-  ( x  =  w  ->  ( A. w  -.  ph  ->  A. x ( x  =  w  ->  -.  ph )
) )
52, 3, 4syl2im 34 . . . . . 6  |-  ( w  =  x  ->  ( -.  ph  ->  A. x
( x  =  w  ->  -.  ph ) ) )
6 ax9v 1636 . . . . . . 7  |-  -.  A. x  -.  x  =  w
7 con2 108 . . . . . . . 8  |-  ( ( x  =  w  ->  -.  ph )  ->  ( ph  ->  -.  x  =  w ) )
87al2imi 1548 . . . . . . 7  |-  ( A. x ( x  =  w  ->  -.  ph )  ->  ( A. x ph  ->  A. x  -.  x  =  w ) )
96, 8mtoi 169 . . . . . 6  |-  ( A. x ( x  =  w  ->  -.  ph )  ->  -.  A. x ph )
105, 9syl6 29 . . . . 5  |-  ( w  =  x  ->  ( -.  ph  ->  -.  A. x ph ) )
1110con4d 97 . . . 4  |-  ( w  =  x  ->  ( A. x ph  ->  ph )
)
1211con3i 127 . . 3  |-  ( -.  ( A. x ph  ->  ph )  ->  -.  w  =  x )
1312alrimiv 1617 . 2  |-  ( -.  ( A. x ph  ->  ph )  ->  A. w  -.  w  =  x
)
141, 13mt3 171 1  |-  ( A. x ph  ->  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1527
This theorem is referenced by:  ax5o  1717  19.8a  1718  hba1  1719  hbn  1720  hbimd  1721  spimeh  1722  ax6o  1723  equsalhw  1730  19.21h  1731  19.12  1734  cbv3hv  1737  spi  1738  sps  1739  spsd  1740  nfr  1741  19.3  1781  19.21t  1790  19.21bi  1794  19.38  1810  ax12olem3  1870  dvelimv  1879  ax9  1889  hbae  1893  spimt  1914  equveli  1928  ax11b  1935  sb2  1963  a16gb  1990  dfsb2  1995  nfsb4t  2020  sb56  2037  sb6  2038  sbal1  2065  exsb  2069  ax4  2084  mo  2165  mopick  2205  2eu1  2223  nfcr  2411  rsp  2603  ceqex  2898  abidnf  2934  mob2  2945  csbie2t  3125  sbcnestgf  3128  mpteq12f  4096  axrep2  4133  axnulALT  4147  dtru  4201  copsex2t  4253  ssopab2  4290  eusv1  4528  alxfr  4547  iota1  5233  dffv2  5592  fiint  7133  isf32lem9  7987  nd3  8211  axrepnd  8216  axpowndlem2  8220  axacndlem4  8232  fiinopn  16647  ex-natded9.26-2  20807  relexpindlem  24036  fundmpss  24122  frmin  24242  wfrlem5  24260  frrlem5  24285  imonclem  25813  prtlem14  26742  setindtr  27117  pm11.57  27588  pm11.59  27590  ax4567to6  27604  ax4567to7  27605  ax10ext  27606  iotain  27617  pm14.123b  27626  eubi  27636  compneOLD  27643  rexsb  27946  ssralv2  28294  19.41rg  28316  hbexg  28322  a9e2ndeq  28325  ssralv2VD  28642  19.41rgVD  28678  hbimpgVD  28680  hbexgVD  28682  a9e2eqVD  28683  a9e2ndeqVD  28685  vk15.4jVD  28690  a9e2ndeqALT  28708  bnj1294  28850  bnj570  28937  bnj953  28971  bnj1204  29042  bnj1388  29063  ax12conj2  29108  a12study8  29119  ax10lem17ALT  29123  ax10lem18ALT  29124
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
  Copyright terms: Public domain W3C validator