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  1867  cbv3  1874  equveli  1880  sbft  1897  ax11eq  2105  cesare  2216  camestres  2217  calemes  2228  ceqsralv  2753  vtocl2  2777  mosub  2880  sbcth  2935  sbciegf  2952  csbiegf  3049  sbcnestg  3058  csbnestg  3059  csbnest1g  3061  int0  3774  mpteq2ia  3999  mpteq2da  4002  ssopab2i  4185  ordom  4556  relssi  4685  xpidtr  4972  funcnvsn  5154  caovmo  5909  tfrlem7  6285  pssnn  6966  findcard  6982  findcard2  6983  fiint  7018  inf0  7206  axinf2  7225  trcl  7294  axac3  7974  brdom3  8037  axpowndlem2  8100  axpowndlem4  8102  axregndlem2  8105  axinfnd  8108  wfgru  8318  nqerf  8434  fzshftral  10747  uzrdgfni  10899  ltweuz  10902  fclim  11904  issubc  13556  isclati  14063  letsr  14184  distop  16565  fctop  16573  cctop  16575  itgparts  19226  relexpind  23208  hbimg  23334  wfrlem11  23434  frrlem5c  23455  fnsingle  23632  funimage  23641  funpartfun  23655  hftr  23986  allt  24014  alnof  24015  eqintg  24126  axlmp2  24190  axlmp3  24191  xindcls  25163  filnetlem3  25495  unirep  25515  riscer  25785  2rexfrabdioph  26043  3rexfrabdioph  26044  4rexfrabdioph  26045  6rexfrabdioph  26046  7rexfrabdioph  26047  pm11.11  26736  refsum2cnlem1  26875  stoweidlem19  26902  stoweidlem44  26927  stoweidlem61  26944  onfrALTlem5  27097  sbc3orgVD  27414  ordelordALTVD  27430  trsbcVD  27440  undif3VD  27445  sbcssVD  27446  csbingVD  27447  onfrALTlem5VD  27448  onfrALTlem1VD  27453  onfrALTVD  27454  csbsngVD  27456  csbxpgVD  27457  csbresgVD  27458  csbrngVD  27459  csbima12gALTVD  27460  csbunigVD  27461  csbfv12gALTVD  27462  19.41rgVD  27465  unisnALT  27489  bnj1023  27598  bnj1109  27604  bnj907  27783  alimiK  27895  ax4wfK  27905  ax4wK  27906  ax12dgen3K  27933  ax12dgen4K  27934  a12lem1  28034  cdleme31snd  29479  cdleme32fva  29530  cdlemeg46c  29606  cdlemk40  30010
  Copyright terms: Public domain W3C validator