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 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  |-  ( 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  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  stoweidlem35  26918  alrim3con13v  27086  a9e2nd  27114  ax172  27133  19.21a3con13vVD  27415  tratrbVD  27424  ssralv2VD  27429  a9e2ndVD  27471  a9e2ndALT  27494  bnj1096  27600  bnj1350  27644  bnj1351  27645  bnj1352  27646  bnj1468  27664  bnj1000  27759  bnj1311  27840  bnj1445  27860  bnj1523  27887  equidK  27889  alimdvK  27898  a4imvK  27904  ax4wK  27906  19.8vK  27908  cbvalivK  27914  ax6wK  27919  ax7wK  27922  ax11wlemK  27926  ax12wK  27930  ax12o10lem1X  27936  ax12o10lem3X  27938  ax12o10lem3K  27939  equvinvK  27964  ax12olem21K  27975  ax12olem21X  27976  ax12olem22K  27978  ax12olem22X  27979  ax12olem26X  27985  ax12olem27X  27986  ax10lem20X  27993  ax10lem21X  27994  ax10lem24X  27997  ax10X  28001  a16gALTX  28002  ax9X  28006  equvinv  28018  equveliv  28019  a12study4  28021  a12study5rev  28026  ax10lem17ALT  28027  dvelimfALT2  28029  a12study2  28038  a12study10  28040  a12study10n  28041  ax9lem1  28044  ax9lem3  28046  ax9lem6  28049  ax9lem14  28057  ax9lem15  28058  ax9lem17  28060  ax9vax9  28062
  Copyright terms: Public domain W3C validator