MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-gen Structured version   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 26151 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  2086  sbftOLD  2116  ax11eq  2270  cesare  2384  camestres  2385  calemes  2396  ceqsralv  2983  vtocl2  3007  mosub  3112  sbcth  3175  sbciegf  3192  csbiegf  3291  sbcnestg  3300  csbnestg  3301  csbnest1g  3303  int0  4064  mpteq2ia  4291  mpteq2da  4294  ssopab2i  4482  ordom  4854  relssi  4967  xpidtr  5256  funcnvsn  5496  caovmo  6284  tfrlem7  6644  pssnn  7327  findcard  7347  findcard2  7348  fiint  7383  inf0  7576  axinf2  7595  trcl  7664  axac3  8344  brdom3  8406  axpowndlem2  8473  axpowndlem4  8475  axregndlem2  8478  axinfnd  8481  wfgru  8691  nqerf  8807  fzshftral  11134  uzrdgfni  11298  ltweuz  11301  fclim  12347  issubc  14035  isclati  14542  letsr  14672  distop  17060  fctop  17068  cctop  17070  itgparts  19931  ulmdm  20309  disjin  24027  abfmpel  24067  xrsclat  24202  relexpind  25140  hbimg  25437  wfrlem11  25548  frrlem5c  25588  fnsingle  25764  funimage  25773  funpartfun  25788  hftr  26123  allt  26151  alnof  26152  filnetlem3  26409  unirep  26414  riscer  26604  2rexfrabdioph  26856  3rexfrabdioph  26857  4rexfrabdioph  26858  6rexfrabdioph  26859  7rexfrabdioph  26860  pm11.11  27547  refsum2cnlem1  27684  0egra0rgra  28375  onfrALTlem5  28628  sbc3orgVD  28963  ordelordALTVD  28979  trsbcVD  28989  undif3VD  28994  sbcssVD  28995  csbingVD  28996  onfrALTlem5VD  28997  onfrALTlem1VD  29002  onfrALTVD  29003  csbsngVD  29005  csbxpgVD  29006  csbresgVD  29007  csbrngVD  29008  csbima12gALTVD  29009  csbunigVD  29010  csbfv12gALTVD  29011  19.41rgVD  29014  unisnALT  29038  bnj1023  29151  bnj1109  29157  bnj907  29336  spimNEW7  29508  cbv3wAUX7  29517  equveliNEW7  29528  sbftNEW7  29556  cbv3OLD7  29723  cdleme32fva  31234  cdlemeg46c  31310  cdlemk40  31714
  Copyright terms: Public domain W3C validator