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

Axiom ax-gen 1533
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 allt 24840 shows the special case  A. x  T.. Theorem spi 1738 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 1527 1  wff  A. x ph
Colors of variables: wff set class
This axiom is referenced by:  gen2  1534  mpg  1535  mpgbi  1536  mpgbir  1537  hbth  1539  stdpc6  1650  ax12dgen3  1701  spim  1915  cbv3  1922  equveli  1928  sbft  1965  ax11eq  2132  cesare  2246  camestres  2247  calemes  2258  ceqsralv  2815  vtocl2  2839  mosub  2943  sbcth  3005  sbciegf  3022  csbiegf  3121  sbcnestg  3130  csbnestg  3131  csbnest1g  3133  int0  3876  mpteq2ia  4102  mpteq2da  4105  ssopab2i  4292  ordom  4665  relssi  4778  xpidtr  5065  funcnvsn  5297  caovmo  6057  tfrlem7  6399  pssnn  7081  findcard  7097  findcard2  7098  fiint  7133  inf0  7322  axinf2  7341  trcl  7410  axac3  8090  brdom3  8153  axpowndlem2  8220  axpowndlem4  8222  axregndlem2  8225  axinfnd  8228  wfgru  8438  nqerf  8554  fzshftral  10869  uzrdgfni  11021  ltweuz  11024  fclim  12027  issubc  13712  isclati  14219  letsr  14349  distop  16733  fctop  16741  cctop  16743  itgparts  19394  ballotth  23096  rabexgfGS  23171  abfmpel  23219  fzossnn  23278  disjin  23362  esumc  23430  relexpind  24037  hbimg  24166  wfrlem11  24266  frrlem5c  24287  fnsingle  24458  funimage  24467  funpartfun  24481  hftr  24812  allt  24840  alnof  24841  eqintg  24961  axlmp2  25025  axlmp3  25026  xindcls  25997  filnetlem3  26329  unirep  26349  riscer  26619  2rexfrabdioph  26877  3rexfrabdioph  26878  4rexfrabdioph  26879  6rexfrabdioph  26880  7rexfrabdioph  26881  pm11.11  27570  refsum2cnlem1  27708  rrpsscn  27719  dvcosre  27741  stoweidlem19  27768  stoweidlem44  27793  stoweidlem61  27810  onfrALTlem5  28307  sbc3orgVD  28627  ordelordALTVD  28643  trsbcVD  28653  undif3VD  28658  sbcssVD  28659  csbingVD  28660  onfrALTlem5VD  28661  onfrALTlem1VD  28666  onfrALTVD  28667  csbsngVD  28669  csbxpgVD  28670  csbresgVD  28671  csbrngVD  28672  csbima12gALTVD  28673  csbunigVD  28674  csbfv12gALTVD  28675  19.41rgVD  28678  unisnALT  28702  bnj1023  28812  bnj1109  28818  bnj907  28997  a12lem1  29130  cdleme31snd  30575  cdleme32fva  30626  cdlemeg46c  30702  cdlemk40  31106
  Copyright terms: Public domain W3C validator