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

Theorem sp 1728
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 1977.

This theorem shows that our obsolete axiom ax-4 2087 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 1727. It is thought the best we can do using only Tarski's axioms is spw 1679. (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 1645 . 2  |-  -.  A. w  -.  w  =  x
2 equcomi 1664 . . . . . . 7  |-  ( w  =  x  ->  x  =  w )
3 ax-17 1606 . . . . . . 7  |-  ( -. 
ph  ->  A. w  -.  ph )
4 ax-11 1727 . . . . . . 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 1645 . . . . . . 7  |-  -.  A. x  -.  x  =  w
7 con2 108 . . . . . . . 8  |-  ( ( x  =  w  ->  -.  ph )  ->  ( ph  ->  -.  x  =  w ) )
87al2imi 1551 . . . . . . 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 1621 . 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 1530
This theorem is referenced by:  ax5o  1729  19.8a  1730  hba1  1731  hbn  1732  hbimd  1733  spimeh  1734  ax6o  1735  equsalhw  1742  19.21h  1743  19.12  1746  cbv3hv  1749  spi  1750  sps  1751  spsd  1752  nfr  1753  19.3  1793  19.21t  1802  19.21bi  1806  19.38  1822  ax12olem3  1882  ax12  1888  dvelimv  1892  ax9  1902  hbae  1906  spimt  1927  equveli  1941  ax11b  1948  sb2  1976  a16gb  2003  dfsb2  2008  nfsb4t  2033  sb56  2050  sb6  2051  sbal1  2078  exsb  2082  ax4  2097  mo  2178  mopick  2218  2eu1  2236  nfcr  2424  rsp  2616  ceqex  2911  abidnf  2947  mob2  2958  csbie2t  3138  sbcnestgf  3141  mpteq12f  4112  axrep2  4149  axnulALT  4163  dtru  4217  copsex2t  4269  ssopab2  4306  eusv1  4544  alxfr  4563  iota1  5249  dffv2  5608  fiint  7149  isf32lem9  8003  nd3  8227  axrepnd  8232  axpowndlem2  8236  axacndlem4  8248  fiinopn  16663  ex-natded9.26-2  20823  relexpindlem  24051  fundmpss  24193  frmin  24313  wfrlem5  24331  frrlem5  24356  imonclem  25916  prtlem14  26845  setindtr  27220  pm11.57  27691  pm11.59  27693  ax4567to6  27707  ax4567to7  27708  ax10ext  27709  iotain  27720  pm14.123b  27729  eubi  27739  compneOLD  27746  rexsb  28049  ssralv2  28593  19.41rg  28615  hbexg  28621  a9e2ndeq  28624  ssralv2VD  28958  19.41rgVD  28994  hbimpgVD  28996  hbexgVD  28998  a9e2eqVD  28999  a9e2ndeqVD  29001  vk15.4jVD  29006  a9e2ndeqALT  29024  bnj1294  29166  bnj570  29253  bnj953  29287  bnj1204  29358  bnj1388  29379  cbv3hvNEW7  29423  19.12vAUX7  29431  ax12olem3aAUX7  29434  dvelimvNEW7  29439  ax9NEW7  29445  hbaewAUX7  29455  spimtNEW7  29484  equveliNEW7  29503  sb2NEW7  29512  a16gbNEW7  29522  nfsb4twAUX7  29551  sb56NEW7  29568  sb6NEW7  29569  exsbNEW7  29571  sbal1NEW7  29587  ax11bNEW7  29594  dfsb2NEW7  29609  ax7w1AUX7  29615  hbaew0AUX7  29617  ax7w2AUX7  29620  ax7w3AUX7  29621  ax7w7AUX7  29623  ax7w7tAUX7  29626  ax7w4AUX7  29628  19.12OLD7  29640  hbaeOLD7  29662  nfsb4tOLD7  29699  nfsb4tw2AUXOLD7  29700  ax12conj2  29730  a12study8  29741  ax10lem17ALT  29745  ax10lem18ALT  29746
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  ax-11 1727
  Copyright terms: Public domain W3C validator