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

Axiom ax-gen 1700
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 31405 shows the special case 𝑥. Theorem spi 1995 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-gen.1 𝜑
Assertion
Ref Expression
ax-gen 𝑥𝜑

Detailed syntax breakdown of Axiom ax-gen
StepHypRef Expression
1 wph . 2 wff 𝜑
2 vx . 2 setvar 𝑥
31, 2wal 1472 1 wff 𝑥𝜑
Colors of variables: wff setvar class
This axiom is referenced by:  gen2  1701  mpg  1702  mpgbi  1703  mpgbir  1704  hbth  1706  stdpc6  1907  ax13dgen3  1964  cesare  2461  camestres  2462  calemes  2473  ceqsalg  3107  ceqsralv  3111  vtocl2  3138  mosub  3255  sbcth  3321  sbciegf  3338  csbiegf  3427  sbcnestg  3852  csbnestg  3853  csbnest1g  3856  int0OLD  4324  mpteq2ia  4566  mpteq2da  4569  ssopab2i  4822  relssi  5027  xpidtr  5328  funcnvsn  5735  caovmo  6644  ordom  6841  wfrfun  7186  tfrlem7  7241  pssnn  7938  findcard  7959  findcard2  7960  fiint  7997  inf0  8276  axinf2  8295  trcl  8362  axac3  9044  brdom3  9106  axpowndlem4  9176  axregndlem2  9179  axinfnd  9182  wfgru  9392  nqerf  9506  uzrdgfni  12486  ltweuz  12489  trclfvcotr  13455  fclim  13996  letsr  16940  distop  20511  fctop  20519  cctop  20521  ulmdm  23839  0egra0rgra  26202  disjin  28570  disjin2  28571  bnj1023  29951  bnj1109  29957  bnj907  30135  hbimg  30802  frrlem5c  30866  fnsingle  31032  funimage  31041  funpartfun  31056  hftr  31295  filnetlem3  31380  allt  31405  alnof  31406  bj-genr  31611  bj-genl  31612  bj-ax12  31658  bj-ceqsalg0  31903  bj-ceqsalgALT  31905  bj-ceqsalgvALT  31907  bj-vtoclgfALT  32044  vtoclefex  32189  rdgeqoa  32226  riscer  32832  ax12eq  33119  cdleme32fva  34618  dfrcl2  36867  pm11.11  37477  sbc3orgVD  37990  ordelordALTVD  38007  trsbcVD  38017  undif3VD  38022  sbcssgVD  38023  csbingVD  38024  onfrALTlem5VD  38025  onfrALTlem1VD  38030  onfrALTVD  38031  csbsngVD  38033  csbxpgVD  38034  csbresgVD  38035  csbrngVD  38036  csbima12gALTVD  38037  csbunigVD  38038  csbfv12gALTVD  38039  19.41rgVD  38042  unisnALT  38066  refsum2cnlem1  38101  dvnprodlem3  38728  sge00  39163  upgr0eopALT  40433
  Copyright terms: Public domain W3C validator