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 1720
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 32375 shows the special case 𝑥. Theorem spi 2052 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 1479 1 wff 𝑥𝜑
Colors of variables: wff setvar class
This axiom is referenced by:  gen2  1721  mpg  1722  mpgbi  1723  mpgbir  1724  hbth  1727  stdpc6  1955  ax13dgen3  2014  cesare  2567  camestres  2568  calemes  2579  ceqsalg  3225  ceqsralv  3229  vtocl2  3256  mosub  3378  sbcth  3444  sbciegf  3461  csbiegf  3550  sbcnestg  3988  csbnestg  3989  csbnest1g  3992  int0OLD  4482  mpteq2ia  4731  mpteq2da  4734  ssopab2i  4993  relssi  5201  xpidtr  5506  funcnvsn  5924  caovmo  6856  ordom  7059  wfrfun  7410  tfrlem7  7464  pssnn  8163  findcard  8184  findcard2  8185  fiint  8222  inf0  8503  axinf2  8522  trcl  8589  axac3  9271  brdom3  9335  axpowndlem4  9407  axregndlem2  9410  axinfnd  9413  wfgru  9623  nqerf  9737  uzrdgfni  12740  ltweuz  12743  trclfvcotr  13731  fclim  14265  letsr  17208  distop  20780  fctop  20789  cctop  20791  ulmdm  24128  upgr0eopALT  25992  disjin  29371  disjin2  29372  bnj1023  30825  bnj1109  30831  bnj907  31009  hbimg  31689  frrlem5c  31760  fnsingle  32001  funimage  32010  funpartfun  32025  hftr  32264  filnetlem3  32350  allt  32375  alnof  32376  bj-genr  32566  bj-genl  32567  bj-genan  32568  bj-ax12  32609  bj-ceqsalg0  32852  bj-ceqsalgALT  32854  bj-ceqsalgvALT  32856  bj-vtoclgfALT  32996  vtoclefex  33152  rdgeqoa  33189  riscer  33758  ax12eq  34045  cdleme32fva  35544  dfrcl2  37785  pm11.11  38393  sbc3orgVD  38906  ordelordALTVD  38923  trsbcVD  38933  undif3VD  38938  sbcssgVD  38939  csbingVD  38940  onfrALTlem5VD  38941  onfrALTlem1VD  38946  onfrALTVD  38947  csbsngVD  38949  csbxpgVD  38950  csbresgVD  38951  csbrngVD  38952  csbima12gALTVD  38953  csbunigVD  38954  csbfv12gALTVD  38955  19.41rgVD  38958  unisnALT  38982  refsum2cnlem1  39016  mptssid  39266  dvnprodlem3  39926  sge00  40356  sprssspr  41496  spcdvw  42191  setrec2lem2  42206  onsetrec  42216
  Copyright terms: Public domain W3C validator