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

Axiom ax-gen 1536
Description: Rule of Generalization. The postulated inference rule of pure predicate calculus. See e.g. Rule 2 of [Hamilton] p. 74. This rule says that if something is unconditionally true, then it is true for all values of a variable. For example, if we have proved  x  =  x, we can conclude  A. x x  =  x or even  A. y
x  =  x. Theorem a4i 1699 shows we can go the other way also: in other words we can add or remove universal quantifiers from the beginning of any theorem as required. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
ax-g.1  |-  ph
Assertion
Ref Expression
ax-gen  |-  A. x ph

Detailed syntax breakdown of Axiom ax-gen
StepHypRef Expression
1 wph . 2  wff  ph
2 vx . 2  set  x
31, 2wal 1532 1  wff  A. x ph
Colors of variables: wff set class
This axiom is referenced by:  gen2  1541  mpg  1542  mpgbi  1543  mpgbir  1544  hbth  1557  ax4  1691  ax5o  1693  ax5  1695  ax6  1698  stdpc6  1821  a4im  1868  cbv3  1875  equveli  1881  sbft  1898  ax11eq  2108  cesare  2219  camestres  2220  calemes  2231  ceqsralv  2783  vtocl2  2807  mosub  2911  sbcth  2966  sbciegf  2983  csbiegf  3082  sbcnestg  3091  csbnestg  3092  csbnest1g  3094  int0  3836  mpteq2ia  4062  mpteq2da  4065  ssopab2i  4250  ordom  4623  relssi  4752  xpidtr  5039  funcnvsn  5221  caovmo  5977  tfrlem7  6353  pssnn  7035  findcard  7051  findcard2  7052  fiint  7087  inf0  7276  axinf2  7295  trcl  7364  axac3  8044  brdom3  8107  axpowndlem2  8174  axpowndlem4  8176  axregndlem2  8179  axinfnd  8182  wfgru  8392  nqerf  8508  fzshftral  10821  uzrdgfni  10973  ltweuz  10976  fclim  11978  issubc  13660  isclati  14167  letsr  14297  distop  16681  fctop  16689  cctop  16691  itgparts  19342  ballotth  23043  relexpind  23395  hbimg  23521  wfrlem11  23621  frrlem5c  23642  fnsingle  23819  funimage  23828  funpartfun  23842  hftr  24173  allt  24201  alnof  24202  eqintg  24313  axlmp2  24377  axlmp3  24378  xindcls  25350  filnetlem3  25682  unirep  25702  riscer  25972  2rexfrabdioph  26230  3rexfrabdioph  26231  4rexfrabdioph  26232  6rexfrabdioph  26233  7rexfrabdioph  26234  pm11.11  26923  refsum2cnlem1  27062  stoweidlem19  27089  stoweidlem44  27114  stoweidlem61  27131  onfrALTlem5  27344  sbc3orgVD  27661  ordelordALTVD  27677  trsbcVD  27687  undif3VD  27692  sbcssVD  27693  csbingVD  27694  onfrALTlem5VD  27695  onfrALTlem1VD  27700  onfrALTVD  27701  csbsngVD  27703  csbxpgVD  27704  csbresgVD  27705  csbrngVD  27706  csbima12gALTVD  27707  csbunigVD  27708  csbfv12gALTVD  27709  19.41rgVD  27712  unisnALT  27736  bnj1023  27845  bnj1109  27851  bnj907  28030  alimiK  28142  ax4wfK  28152  ax4wK  28153  ax12dgen3K  28180  ax12dgen4K  28181  a12lem1  28281  cdleme31snd  29726  cdleme32fva  29777  cdlemeg46c  29853  cdlemk40  30257
  Copyright terms: Public domain W3C validator