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

Axiom ax-gen 1555
Description: Rule of Generalization. The postulated inference rule of 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 26143 shows the special case  A. x  T.. Theorem spi 1769 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 1549 1  wff  A. x ph
Colors of variables: wff set class
This axiom is referenced by:  gen2  1556  mpg  1557  mpgbi  1558  mpgbir  1559  hbth  1561  stdpc6  1699  ax12dgen3  1742  spimOLD  1958  cbv3OLD  1978  equveliOLD  2082  sbftOLD  2104  ax11eq  2269  cesare  2383  camestres  2384  calemes  2395  ceqsralv  2975  vtocl2  2999  mosub  3104  sbcth  3167  sbciegf  3184  csbiegf  3283  sbcnestg  3292  csbnestg  3293  csbnest1g  3295  int0  4056  mpteq2ia  4283  mpteq2da  4286  ssopab2i  4474  ordom  4846  relssi  4959  xpidtr  5248  funcnvsn  5488  caovmo  6276  tfrlem7  6636  pssnn  7319  findcard  7339  findcard2  7340  fiint  7375  inf0  7568  axinf2  7587  trcl  7656  axac3  8336  brdom3  8398  axpowndlem2  8465  axpowndlem4  8467  axregndlem2  8470  axinfnd  8473  wfgru  8683  nqerf  8799  fzshftral  11126  uzrdgfni  11290  ltweuz  11293  fclim  12339  issubc  14027  isclati  14534  letsr  14664  distop  17052  fctop  17060  cctop  17062  itgparts  19923  ulmdm  20301  disjin  24019  abfmpel  24059  xrsclat  24194  relexpind  25132  hbimg  25429  wfrlem11  25540  frrlem5c  25580  fnsingle  25756  funimage  25765  funpartfun  25780  hftr  26115  allt  26143  alnof  26144  filnetlem3  26400  unirep  26405  riscer  26595  2rexfrabdioph  26847  3rexfrabdioph  26848  4rexfrabdioph  26849  6rexfrabdioph  26850  7rexfrabdioph  26851  pm11.11  27538  refsum2cnlem1  27675  onfrALTlem5  28565  sbc3orgVD  28900  ordelordALTVD  28916  trsbcVD  28926  undif3VD  28931  sbcssVD  28932  csbingVD  28933  onfrALTlem5VD  28934  onfrALTlem1VD  28939  onfrALTVD  28940  csbsngVD  28942  csbxpgVD  28943  csbresgVD  28944  csbrngVD  28945  csbima12gALTVD  28946  csbunigVD  28947  csbfv12gALTVD  28948  19.41rgVD  28951  unisnALT  28975  bnj1023  29088  bnj1109  29094  bnj907  29273  spimNEW7  29445  cbv3wAUX7  29454  equveliNEW7  29465  sbftNEW7  29493  cbv3OLD7  29660  cdleme32fva  31171  cdlemeg46c  31247  cdlemk40  31651
  Copyright terms: Public domain W3C validator