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

Axiom ax-gen 1618
 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 29866 shows the special case . Theorem spi 1864 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, 3-Jan-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 1393 1
 Colors of variables: wff setvar class This axiom is referenced by:  gen2  1619  mpg  1620  mpgbi  1621  mpgbir  1622  hbth  1624  stdpc6  1800  ax13dgen3  1835  ax12eq  2271  cesare  2402  camestres  2403  calemes  2414  ceqsalg  3134  ceqsralv  3138  vtocl2  3162  mosub  3277  sbcth  3342  sbciegf  3359  csbiegf  3458  sbcnestg  3841  csbnestg  3842  csbnest1g  3845  int0  4300  mpteq2ia  4534  mpteq2da  4537  ssopab2i  4780  relssi  5099  xpidtr  5394  funcnvsn  5638  caovmo  6512  ordom  6709  tfrlem7  7071  pssnn  7758  findcard  7779  findcard2  7780  fiint  7817  inf0  8059  axinf2  8078  trcl  8180  axac3  8865  brdom3  8927  axpowndlem2OLD  8995  axpowndlem4  8998  axregndlem2  9001  axinfnd  9005  wfgru  9215  nqerf  9329  uzrdgfni  12069  ltweuz  12072  fclim  13376  letsr  15857  distop  19497  fctop  19505  cctop  19507  ulmdm  22788  0egra0rgra  24936  disjin  27446  relexpind  29063  hbimg  29242  wfrlem11  29353  frrlem5c  29393  fnsingle  29569  funimage  29578  funpartfun  29593  hftr  29839  allt  29866  alnof  29867  filnetlem3  30198  riscer  30391  pm11.11  31279  refsum2cnlem1  31412  dvnprodlem3  31745  sbc3orgVD  33651  ordelordALTVD  33667  trsbcVD  33677  undif3VD  33682  sbcssgVD  33683  csbingVD  33684  onfrALTlem5VD  33685  onfrALTlem1VD  33690  onfrALTVD  33691  csbsngVD  33693  csbxpgVD  33694  csbresgVD  33695  csbrngVD  33696  csbima12gALTVD  33697  csbunigVD  33698  csbfv12gALTVD  33699  19.41rgVD  33702  unisnALT  33726  bnj1023  33839  bnj1109  33845  bnj907  34023  bj-alrimih  34209  bj-ceqsalg0  34453  bj-ceqsalgALT  34455  bj-ceqsalgvALT  34457  bj-vtoclgfALT  34588  cdleme32fva  36163
 Copyright terms: Public domain W3C validator