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

Axiom ax-gen 1570
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 , we can conclude or even . Theorem allt 27490 shows the special case . Theorem spi 1775 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
Assertion
Ref Expression
ax-gen

Detailed syntax breakdown of Axiom ax-gen
StepHypRef Expression
1 wph . 2
2 vx . 2
31, 2wal 1564 1
Colors of variables: wff set class
This axiom is referenced by:  gen2  1571  mpg  1572  mpgbi  1573  mpgbir  1574  hbth  1576  stdpc6  1715  ax13dgen3  1749  spimOLD  1965  cbv3OLD  1985  equveliOLD  2094  sbftOLD  2126  ax12eq  2302  cesare  2437  camestres  2438  calemes  2449  ceqsralv  3042  vtocl2  3066  mosub  3175  sbcth  3238  sbciegf  3255  csbiegf  3349  sbcnestg  3728  csbnestg  3729  csbnest1g  3732  int0  4168  mpteq2ia  4400  mpteq2da  4403  ssopab2i  4639  relssi  4953  xpidtr  5243  funcnvsn  5481  caovmo  6310  ordom  6495  tfrlem7  6806  pssnn  7492  findcard  7512  findcard2  7513  fiint  7549  inf0  7743  axinf2  7762  trcl  7831  axac3  8515  brdom3  8577  axpowndlem2  8644  axpowndlem4  8646  axregndlem2  8649  axinfnd  8652  wfgru  8862  nqerf  8978  uzrdgfni  11630  ltweuz  11633  fclim  12878  letsr  15238  distop  18074  fctop  18082  cctop  18084  ulmdm  21324  disjin  25057  relexpind  26482  hbimg  26776  wfrlem11  26887  frrlem5c  26927  fnsingle  27103  funimage  27112  funpartfun  27127  hftr  27462  allt  27490  alnof  27491  filnetlem3  27781  riscer  27976  pm11.11  28800  refsum2cnlem1  28934  0egra0rgra  29730  sbc3orgVD  30433  ordelordALTVD  30449  trsbcVD  30459  undif3VD  30464  sbcssgVD  30465  csbingVD  30466  onfrALTlem5VD  30467  onfrALTlem1VD  30472  onfrALTVD  30473  csbsngVD  30475  csbxpgVD  30476  csbresgVD  30477  csbrngVD  30478  csbima12gALTVD  30479  csbunigVD  30480  csbfv12gALTVD  30481  19.41rgVD  30484  unisnALT  30508  bnj1023  30621  bnj1109  30627  bnj907  30806  spimNEW11  31060  cbv3wAUX11  31069  equveliNEW11  31080  sbftNEW11  31108  cbv3OLD11  31274  cdleme32fva  32784
  Copyright terms: Public domain W3C validator