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

Axiom ax-17 1628
Description: Axiom to quantify a variable over a formula in which it does not occur. Axiom C5 in [Megill] p. 444 (p. 11 of the preprint). Also appears as Axiom B6 (p. 75) of system S2 of [Tarski] p. 77 and Axiom C5-1 of [Monk2] p. 113.

This axiom is logically redundant in the (logically complete) predicate calculus axiom system consisting of ax-gen 1536, ax-4 1692 through ax-9 1684, ax-10o 1836, and ax-12o 1664 through ax-16 1927: in that system, we can derive any instance of ax-17 1628 not containing wff variables by induction on formula length, using ax17eq 1928 and ax17el 2106 for the basis together hbn 1722, hbal 1567, and hbim 1723. However, if we omit this axiom, our development would be quite inconvenient since we could work only with specific instances of wffs containing no wff variables - this axiom introduces the concept of a set variable not occurring in a wff (as opposed to just two set variables being distinct). (Contributed by NM, 5-Aug-1993.)

Assertion
Ref Expression
ax-17  |-  ( ph  ->  A. x ph )
Distinct variable group:    ph, x

Detailed syntax breakdown of Axiom ax-17
StepHypRef Expression
1 wph . 2  wff  ph
2 vx . . 3  set  x
31, 2wal 1532 . 2  wff  A. x ph
41, 3wi 6 1  wff  ( ph  ->  A. x ph )
Colors of variables: wff set class
This axiom is referenced by:  nfv  1629  a17d  1630  ax12o10lem1  1635  ax12o10lem3  1637  ax12olem21  1655  ax12olem22  1656  ax12olem26  1660  ax12olem27  1661  ax10lem20  1669  ax10lem21  1670  ax10lem24  1673  ax10  1677  a16gALT  1679  ax9  1683  ax4  1691  equid1  1820  dveeq2  1929  dveeq2-o  1930  ax11a2  1938  ax11a2-o  1939  ax16ALT  1996  cleljust  2063  dvelim  2095  dvelimALT  2097  dveeq1  2098  dveeq1-o  2099  dveel1  2101  dveel2  2102  ax15  2104  ax11el  2109  eujustALT  2120  cleqh  2353  abeq2  2361  rgen2a  2582  mpteq12  4059  stoweidlem35  27105  alrim3con13v  27333  a9e2nd  27361  ax172  27380  19.21a3con13vVD  27662  tratrbVD  27671  ssralv2VD  27676  a9e2ndVD  27718  a9e2ndALT  27741  bnj1096  27847  bnj1350  27891  bnj1351  27892  bnj1352  27893  bnj1468  27911  bnj1000  28006  bnj1311  28087  bnj1445  28107  bnj1523  28134  equidK  28136  alimdvK  28145  a4imvK  28151  ax4wK  28153  19.8vK  28155  cbvalivK  28161  ax6wK  28166  ax7wK  28169  ax11wlemK  28173  ax12wK  28177  ax12o10lem1X  28183  ax12o10lem3X  28185  ax12o10lem3K  28186  equvinvK  28211  ax12olem21K  28222  ax12olem21X  28223  ax12olem22K  28225  ax12olem22X  28226  ax12olem26X  28232  ax12olem27X  28233  ax10lem20X  28240  ax10lem21X  28241  ax10lem24X  28244  ax10X  28248  a16gALTX  28249  ax9X  28253  equvinv  28265  equveliv  28266  a12study4  28268  a12study5rev  28273  ax10lem17ALT  28274  dvelimfALT2  28276  a12study2  28285  a12study10  28287  a12study10n  28288  ax9lem1  28291  ax9lem3  28293  ax9lem6  28296  ax9lem14  28304  ax9lem15  28305  ax9lem17  28307  ax9vax9  28309
  Copyright terms: Public domain W3C validator