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

Axiom ax-gen 1556
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 ?Error: = x ^ This math symbol is not active (i.e. was not declared in this scope). variable. For example, if we have proved = , we can conclude ?Error: = x ^ This math symbol is not active (i.e. was not declared in this scope). ?Error: = x ^ This math symbol is not active (i.e. was not declared in this scope). A. = or even A. = . Theorem allt 26255 shows the special case . Theorem spi 1772 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 1550 1
Colors of variables: wff set class
This axiom is referenced by:  gen2  1557  mpg  1558  mpgbi  1559  mpgbir  1560  hbth  1562  stdpc6  1702  ax12dgen3  1745  spimOLD  1962  cbv3OLD  1982  equveliOLD  2090  sbftOLD  2121  ax11eq  2277  cesare  2391  camestres  2392  calemes  2403  ceqsralv  2992  vtocl2  3016  mosub  3121  sbcth  3184  sbciegf  3201  csbiegf  3293  sbcnestg  3671  csbnestg  3672  csbnest1g  3675  int0  4093  mpteq2ia  4325  mpteq2da  4328  ssopab2i  4521  ordom  4895  relssi  5009  xpidtr  5300  funcnvsn  5543  caovmo  6334  tfrlem7  6693  pssnn  7376  findcard  7396  findcard2  7397  fiint  7432  inf0  7625  axinf2  7644  trcl  7713  axac3  8395  brdom3  8457  axpowndlem2  8524  axpowndlem4  8526  axregndlem2  8529  axinfnd  8532  wfgru  8742  nqerf  8858  uzrdgfni  11349  ltweuz  11352  fclim  12398  isclati  14593  letsr  14723  distop  17111  fctop  17119  cctop  17121  ulmdm  20360  disjin  24076  xrsclat  24251  relexpind  25244  hbimg  25541  wfrlem11  25652  frrlem5c  25692  fnsingle  25868  funimage  25877  funpartfun  25892  hftr  26227  allt  26255  alnof  26256  filnetlem3  26520  riscer  26715  pm11.11  27726  refsum2cnlem1  27862  0egra0rgra  28611  sbc3orgVD  29204  ordelordALTVD  29220  trsbcVD  29230  undif3VD  29235  sbcssgVD  29236  csbingVD  29237  onfrALTlem5VD  29238  onfrALTlem1VD  29243  onfrALTVD  29244  csbsngVD  29246  csbxpgVD  29247  csbresgVD  29248  csbrngVD  29249  csbima12gALTVD  29250  csbunigVD  29251  csbfv12gALTVD  29252  19.41rgVD  29255  unisnALT  29279  bnj1023  29392  bnj1109  29398  bnj907  29577  spimNEW7  29749  cbv3wAUX7  29758  equveliNEW7  29769  sbftNEW7  29797  cbv3OLD7  29964  cdleme32fva  31474
  Copyright terms: Public domain W3C validator