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

Axiom ax-gen 1535
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 24249 shows the special case  A. x  T.. Theorem spi 1742 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 1529 1  wff  A. x ph
Colors of variables: wff set class
This axiom is referenced by:  gen2  1536  mpg  1537  mpgbi  1538  mpgbir  1539  hbth  1541  stdpc6  1653  ax12dgen3  1704  spim  1920  cbv3  1927  equveli  1933  sbft  1972  ax11eq  2135  cesare  2249  camestres  2250  calemes  2261  ceqsralv  2818  vtocl2  2842  mosub  2946  sbcth  3008  sbciegf  3025  csbiegf  3124  sbcnestg  3133  csbnestg  3134  csbnest1g  3136  int0  3879  mpteq2ia  4105  mpteq2da  4108  ssopab2i  4293  ordom  4666  relssi  4779  xpidtr  5066  funcnvsn  5264  caovmo  6020  tfrlem7  6396  pssnn  7078  findcard  7094  findcard2  7095  fiint  7130  inf0  7319  axinf2  7338  trcl  7407  axac3  8087  brdom3  8150  axpowndlem2  8217  axpowndlem4  8219  axregndlem2  8222  axinfnd  8225  wfgru  8435  nqerf  8551  fzshftral  10865  uzrdgfni  11017  ltweuz  11020  fclim  12023  issubc  13708  isclati  14215  letsr  14345  distop  16729  fctop  16737  cctop  16739  itgparts  19390  ballotth  23091  relexpind  23443  hbimg  23569  wfrlem11  23669  frrlem5c  23690  fnsingle  23867  funimage  23876  funpartfun  23890  hftr  24221  allt  24249  alnof  24250  eqintg  24361  axlmp2  24425  axlmp3  24426  xindcls  25398  filnetlem3  25730  unirep  25750  riscer  26020  2rexfrabdioph  26278  3rexfrabdioph  26279  4rexfrabdioph  26280  6rexfrabdioph  26281  7rexfrabdioph  26282  pm11.11  26971  refsum2cnlem1  27109  rrpsscn  27120  dvcosre  27142  stoweidlem19  27169  stoweidlem44  27194  stoweidlem61  27211  onfrALTlem5  27580  sbc3orgVD  27897  ordelordALTVD  27913  trsbcVD  27923  undif3VD  27928  sbcssVD  27929  csbingVD  27930  onfrALTlem5VD  27931  onfrALTlem1VD  27936  onfrALTVD  27937  csbsngVD  27939  csbxpgVD  27940  csbresgVD  27941  csbrngVD  27942  csbima12gALTVD  27943  csbunigVD  27944  csbfv12gALTVD  27945  19.41rgVD  27948  unisnALT  27972  bnj1023  28081  bnj1109  28087  bnj907  28266  a12lem1  28399  cdleme31snd  29844  cdleme32fva  29895  cdlemeg46c  29971  cdlemk40  30375
  Copyright terms: Public domain W3C validator