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

Axiom ax-gen 1556
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 26156 shows the special case  A. x  T.. Theorem spi 1770 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 1550 1  wff  A. x ph
Colors of variables: wff set class
This axiom is referenced by:  gen2  1557  mpg  1558  mpgbi  1559  mpgbir  1560  hbth  1562  stdpc6  1700  ax12dgen3  1743  spimOLD  1959  cbv3OLD  1979  equveliOLD  2087  sbftOLD  2118  ax11eq  2272  cesare  2386  camestres  2387  calemes  2398  ceqsralv  2985  vtocl2  3009  mosub  3114  sbcth  3177  sbciegf  3194  csbiegf  3293  sbcnestg  3302  csbnestg  3303  csbnest1g  3305  int0  4066  mpteq2ia  4294  mpteq2da  4297  ssopab2i  4485  ordom  4857  relssi  4970  xpidtr  5259  funcnvsn  5499  caovmo  6287  tfrlem7  6647  pssnn  7330  findcard  7350  findcard2  7351  fiint  7386  inf0  7579  axinf2  7598  trcl  7667  axac3  8349  brdom3  8411  axpowndlem2  8478  axpowndlem4  8480  axregndlem2  8483  axinfnd  8486  wfgru  8696  nqerf  8812  fzshftral  11139  uzrdgfni  11303  ltweuz  11306  fclim  12352  issubc  14040  isclati  14547  letsr  14677  distop  17065  fctop  17073  cctop  17075  itgparts  19936  ulmdm  20314  disjin  24032  abfmpel  24072  xrsclat  24207  relexpind  25145  hbimg  25442  wfrlem11  25553  frrlem5c  25593  fnsingle  25769  funimage  25778  funpartfun  25793  hftr  26128  allt  26156  alnof  26157  filnetlem3  26423  unirep  26428  riscer  26618  2rexfrabdioph  26870  3rexfrabdioph  26871  4rexfrabdioph  26872  6rexfrabdioph  26873  7rexfrabdioph  26874  pm11.11  27561  refsum2cnlem1  27698  0egra0rgra  28447  onfrALTlem5  28702  sbc3orgVD  29037  ordelordALTVD  29053  trsbcVD  29063  undif3VD  29068  sbcssVD  29069  csbingVD  29070  onfrALTlem5VD  29071  onfrALTlem1VD  29076  onfrALTVD  29077  csbsngVD  29079  csbxpgVD  29080  csbresgVD  29081  csbrngVD  29082  csbima12gALTVD  29083  csbunigVD  29084  csbfv12gALTVD  29085  19.41rgVD  29088  unisnALT  29112  bnj1023  29225  bnj1109  29231  bnj907  29410  spimNEW7  29582  cbv3wAUX7  29591  equveliNEW7  29602  sbftNEW7  29630  cbv3OLD7  29797  cdleme32fva  31308  cdlemeg46c  31384  cdlemk40  31788
  Copyright terms: Public domain W3C validator