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 1835, and ax-12o 1664 through ax-16 1926: in that system, we can derive any instance of ax-17 1628 not containing wff variables by induction on formula length, using ax17eq 1927 and ax17el 2103 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
Distinct variable group:   ,

Detailed syntax breakdown of Axiom ax-17
StepHypRef Expression
1 wph . 2
2 vx . . 3
31, 2wal 1532 . 2
41, 3wi 6 1
 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  1928  dveeq2-o  1929  ax11a2  1937  ax11a2-o  1938  ax16ALT  1995  cleljust  2060  dvelim  2092  dvelimALT  2094  dveeq1  2095  dveeq1-o  2096  dveel1  2098  dveel2  2099  ax15  2101  ax11el  2106  eujustALT  2117  cleqh  2346  abeq2  2354  rgen2a  2571  mpteq12  3996  alrim3con13v  26989  a9e2nd  27017  ax172  27036  19.21a3con13vVD  27318  tratrbVD  27327  ssralv2VD  27332  a9e2ndVD  27374  a9e2ndALT  27397  bnj1096  27503  bnj1350  27547  bnj1351  27548  bnj1352  27549  bnj1468  27567  bnj1000  27662  bnj1311  27743  bnj1445  27763  bnj1523  27790  equvinv  27803  equveliv  27804  a12study4  27806  a12study5rev  27811  ax10lem17ALT  27812  dvelimfALT2  27814  a12study2  27823  a12study10  27825  a12study10n  27826  ax9lem1  27829  ax9lem3  27831  ax9lem6  27834  ax9lem14  27842  ax9lem15  27843  ax9lem17  27845  ax9vax9  27847
 Copyright terms: Public domain W3C validator