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

Axiom ax-gen 1552
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 26055 shows the special case  A. x  T.. Theorem spi 1765 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 1546 1  wff  A. x ph
Colors of variables: wff set class
This axiom is referenced by:  gen2  1553  mpg  1554  mpgbi  1555  mpgbir  1556  hbth  1558  stdpc6  1695  ax12dgen3  1738  spimOLD  1956  cbv3  2035  equveliOLD  2043  sbft  2074  ax11eq  2243  cesare  2357  camestres  2358  calemes  2369  ceqsralv  2943  vtocl2  2967  mosub  3072  sbcth  3135  sbciegf  3152  csbiegf  3251  sbcnestg  3260  csbnestg  3261  csbnest1g  3263  int0  4024  mpteq2ia  4251  mpteq2da  4254  ssopab2i  4442  ordom  4813  relssi  4926  xpidtr  5215  funcnvsn  5455  caovmo  6243  tfrlem7  6603  pssnn  7286  findcard  7306  findcard2  7307  fiint  7342  inf0  7532  axinf2  7551  trcl  7620  axac3  8300  brdom3  8362  axpowndlem2  8429  axpowndlem4  8431  axregndlem2  8434  axinfnd  8437  wfgru  8647  nqerf  8763  fzshftral  11089  uzrdgfni  11253  ltweuz  11256  fclim  12302  issubc  13990  isclati  14497  letsr  14627  distop  17015  fctop  17023  cctop  17025  itgparts  19884  ulmdm  20262  disjin  23980  abfmpel  24020  xrsclat  24155  relexpind  25093  hbimg  25380  wfrlem11  25480  frrlem5c  25501  fnsingle  25672  funimage  25681  funpartfun  25696  hftr  26027  allt  26055  alnof  26056  filnetlem3  26299  unirep  26304  riscer  26494  2rexfrabdioph  26746  3rexfrabdioph  26747  4rexfrabdioph  26748  6rexfrabdioph  26749  7rexfrabdioph  26750  pm11.11  27438  refsum2cnlem1  27575  onfrALTlem5  28339  sbc3orgVD  28672  ordelordALTVD  28688  trsbcVD  28698  undif3VD  28703  sbcssVD  28704  csbingVD  28705  onfrALTlem5VD  28706  onfrALTlem1VD  28711  onfrALTVD  28712  csbsngVD  28714  csbxpgVD  28715  csbresgVD  28716  csbrngVD  28717  csbima12gALTVD  28718  csbunigVD  28719  csbfv12gALTVD  28720  19.41rgVD  28723  unisnALT  28747  bnj1023  28857  bnj1109  28863  bnj907  29042  spimNEW7  29214  cbv3wAUX7  29221  equveliNEW7  29232  sbftNEW7  29260  cbv3OLD7  29407  cdleme32fva  30919  cdlemeg46c  30995  cdlemk40  31399
  Copyright terms: Public domain W3C validator