MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-gen 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 26099 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  4845  relssi  4958  xpidtr  5247  funcnvsn  5487  caovmo  6275  tfrlem7  6635  pssnn  7318  findcard  7338  findcard2  7339  fiint  7374  inf0  7565  axinf2  7584  trcl  7653  axac3  8333  brdom3  8395  axpowndlem2  8462  axpowndlem4  8464  axregndlem2  8467  axinfnd  8470  wfgru  8680  nqerf  8796  fzshftral  11122  uzrdgfni  11286  ltweuz  11289  fclim  12335  issubc  14023  isclati  14530  letsr  14660  distop  17048  fctop  17056  cctop  17058  itgparts  19919  ulmdm  20297  disjin  24015  abfmpel  24055  xrsclat  24190  relexpind  25128  hbimg  25421  wfrlem11  25521  frrlem5c  25542  fnsingle  25714  funimage  25723  funpartfun  25738  hftr  26071  allt  26099  alnof  26100  filnetlem3  26346  unirep  26351  riscer  26541  2rexfrabdioph  26793  3rexfrabdioph  26794  4rexfrabdioph  26795  6rexfrabdioph  26796  7rexfrabdioph  26797  pm11.11  27485  refsum2cnlem1  27622  onfrALTlem5  28483  sbc3orgVD  28817  ordelordALTVD  28833  trsbcVD  28843  undif3VD  28848  sbcssVD  28849  csbingVD  28850  onfrALTlem5VD  28851  onfrALTlem1VD  28856  onfrALTVD  28857  csbsngVD  28859  csbxpgVD  28860  csbresgVD  28861  csbrngVD  28862  csbima12gALTVD  28863  csbunigVD  28864  csbfv12gALTVD  28865  19.41rgVD  28868  unisnALT  28892  bnj1023  29005  bnj1109  29011  bnj907  29190  spimNEW7  29362  cbv3wAUX7  29369  equveliNEW7  29380  sbftNEW7  29408  cbv3OLD7  29562  cdleme32fva  31073  cdlemeg46c  31149  cdlemk40  31553
  Copyright terms: Public domain W3C validator