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  onfrALTlem5  27000  sbc3orgVD  27317  ordelordALTVD  27333  trsbcVD  27343  undif3VD  27348  sbcssVD  27349  csbingVD  27350  onfrALTlem5VD  27351  onfrALTlem1VD  27356  onfrALTVD  27357  csbsngVD  27359  csbxpgVD  27360  csbresgVD  27361  csbrngVD  27362  csbima12gALTVD  27363  csbunigVD  27364  csbfv12gALTVD  27365  19.41rgVD  27368  unisnALT  27392  bnj1023  27501  bnj1109  27507  bnj907  27686  a12lem1  27819  cdleme31snd  29264  cdleme32fva  29315  cdlemeg46c  29391  cdlemk40  29795
  Copyright terms: Public domain W3C validator