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 allt 24912 shows the special case  A. x  T.. Theorem spi 1750 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 1530 1  wff  A. x ph
Colors of variables: wff set class
This axiom is referenced by:  gen2  1537  mpg  1538  mpgbi  1539  mpgbir  1540  hbth  1542  stdpc6  1670  ax12dgen3  1713  spim  1928  cbv3  1935  equveli  1941  sbft  1978  ax11eq  2145  cesare  2259  camestres  2260  calemes  2271  ceqsralv  2828  vtocl2  2852  mosub  2956  sbcth  3018  sbciegf  3035  csbiegf  3134  sbcnestg  3143  csbnestg  3144  csbnest1g  3146  int0  3892  mpteq2ia  4118  mpteq2da  4121  ssopab2i  4308  ordom  4681  relssi  4794  xpidtr  5081  funcnvsn  5313  caovmo  6073  tfrlem7  6415  pssnn  7097  findcard  7113  findcard2  7114  fiint  7149  inf0  7338  axinf2  7357  trcl  7426  axac3  8106  brdom3  8169  axpowndlem2  8236  axpowndlem4  8238  axregndlem2  8241  axinfnd  8244  wfgru  8454  nqerf  8570  fzshftral  10885  uzrdgfni  11037  ltweuz  11040  fclim  12043  issubc  13728  isclati  14235  letsr  14365  distop  16749  fctop  16757  cctop  16759  itgparts  19410  ballotth  23112  rabexgfGS  23187  abfmpel  23234  fzossnn  23293  disjin  23377  esumc  23445  relexpind  24052  hbimg  24237  wfrlem11  24337  frrlem5c  24358  fnsingle  24529  funimage  24538  funpartfun  24553  hftr  24884  allt  24912  alnof  24913  eqintg  25064  axlmp2  25128  axlmp3  25129  xindcls  26100  filnetlem3  26432  unirep  26452  riscer  26722  2rexfrabdioph  26980  3rexfrabdioph  26981  4rexfrabdioph  26982  6rexfrabdioph  26983  7rexfrabdioph  26984  pm11.11  27673  refsum2cnlem1  27811  rrpsscn  27822  dvcosre  27844  stoweidlem19  27871  stoweidlem44  27896  stoweidlem61  27913  onfrALTlem5  28606  sbc3orgVD  28943  ordelordALTVD  28959  trsbcVD  28969  undif3VD  28974  sbcssVD  28975  csbingVD  28976  onfrALTlem5VD  28977  onfrALTlem1VD  28982  onfrALTVD  28983  csbsngVD  28985  csbxpgVD  28986  csbresgVD  28987  csbrngVD  28988  csbima12gALTVD  28989  csbunigVD  28990  csbfv12gALTVD  28991  19.41rgVD  28994  unisnALT  29018  bnj1023  29128  bnj1109  29134  bnj907  29313  spimNEW7  29485  cbv3wAUX7  29492  equveliNEW7  29503  sbftNEW7  29531  cbv3OLD7  29677  a12lem1  29752  cdleme31snd  31197  cdleme32fva  31248  cdlemeg46c  31324  cdlemk40  31728
  Copyright terms: Public domain W3C validator