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

Axiom ax-gen 1562
 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 26981 shows the special case . Theorem spi 1767 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 1556 1
 Colors of variables: wff set class This axiom is referenced by:  gen2  1563  mpg  1564  mpgbi  1565  mpgbir  1566  hbth  1568  stdpc6  1707  ax13dgen3  1741  spimOLD  1957  cbv3OLD  1977  equveliOLD  2086  sbftOLD  2118  ax12eq  2294  cesare  2429  camestres  2430  calemes  2441  ceqsralv  3033  vtocl2  3057  mosub  3163  sbcth  3226  sbciegf  3243  csbiegf  3337  sbcnestg  3715  csbnestg  3716  csbnest1g  3719  int0  4152  mpteq2ia  4384  mpteq2da  4387  ssopab2i  4621  relssi  4935  xpidtr  5222  funcnvsn  5460  caovmo  6267  ordom  6450  tfrlem7  6756  pssnn  7439  findcard  7459  findcard2  7460  fiint  7495  inf0  7688  axinf2  7707  trcl  7776  axac3  8458  brdom3  8520  axpowndlem2  8587  axpowndlem4  8589  axregndlem2  8592  axinfnd  8595  wfgru  8805  nqerf  8921  uzrdgfni  11573  ltweuz  11576  fclim  12817  letsr  15175  distop  17563  fctop  17571  cctop  17573  ulmdm  20813  disjin  24548  relexpind  25973  hbimg  26267  wfrlem11  26378  frrlem5c  26418  fnsingle  26594  funimage  26603  funpartfun  26618  hftr  26953  allt  26981  alnof  26982  filnetlem3  27272  riscer  27467  pm11.11  28475  refsum2cnlem1  28609  0egra0rgra  29408  sbc3orgVD  30156  ordelordALTVD  30172  trsbcVD  30182  undif3VD  30187  sbcssgVD  30188  csbingVD  30189  onfrALTlem5VD  30190  onfrALTlem1VD  30195  onfrALTVD  30196  csbsngVD  30198  csbxpgVD  30199  csbresgVD  30200  csbrngVD  30201  csbima12gALTVD  30202  csbunigVD  30203  csbfv12gALTVD  30204  19.41rgVD  30207  unisnALT  30231  bnj1023  30344  bnj1109  30350  bnj907  30529  spimNEW11  30783  cbv3wAUX11  30792  equveliNEW11  30803  sbftNEW11  30831  cbv3OLD11  30997  cdleme32fva  32507
 Copyright terms: Public domain W3C validator