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 1790
Description: Rule of (universal) generalization. In our axiomatization, this is the only postulated (that is, axiomatic) rule of inference of predicate calculus (together with the rule of modus ponens ax-mp 5 of propositional 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 𝑥 = 𝑥, then we can conclude 𝑥𝑥 = 𝑥 or even 𝑦𝑥 = 𝑥. Theorem altru 1802 shows the special case 𝑥. The converse rule of inference spi 2180 (universal instantiation, or universal specialization) shows that we can also go the other way: in other words, we can add or remove universal quantifiers from the beginning of any theorem as required. Note that the closed form (𝜑 → ∀𝑥𝜑) need not hold (but may hold in special cases, see ax-5 1906). (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 1533 1 wff 𝑥𝜑
Colors of variables: wff setvar class
This axiom is referenced by:  gen2  1791  mpg  1792  mpgbi  1793  mpgbir  1794  hbth  1798  altru  1802  alfal  1803  stdpc6  2023  sbt  2062  ax13dgen3  2135  ceqsalg  3514  vtoclegft  3588  mosub  3722  sbcth  3806  sbciegf  3831  sbcg  3870  csbiegf  3942  sbcnestgw  4429  csbnestgw  4430  sbcnestg  4434  csbnestg  4435  csbnest1g  4438  mpteq2daOLD  5249  mpteq2iaOLD  5254  al0ssb  5310  intidg  5461  ssopab2i  5553  relssi  5795  xpidtr  6140  funcnvsn  6614  caovmo  7665  trom  7890  peano1  7905  abrexexg  7979  wfrfunOLD  8353  tfrlem7  8417  1onn  8672  2onn  8674  findcard  9197  findcard2  9198  pssnn  9202  ssfi  9207  fiint  9359  fiintOLD  9360  inf0  9653  axinf2  9672  trcl  9760  axac3  10496  brdom3  10560  axpowndlem4  10632  axregndlem2  10635  axinfnd  10638  wfgru  10848  nqerf  10962  uzrdgfni  13986  ltweuz  13989  trclfvcotr  15035  fclim  15576  letsr  18640  cnsubrglem  21434  distop  23000  fctop  23009  cctop  23011  ulmdm  26433  upgr0eopALT  29130  bnj1023  34734  bnj1109  34740  bnj907  34921  funen1cnv  35042  axnulg  35046  loop1cycl  35083  umgr2cycl  35087  hbimg  35751  fnsingle  35861  funimage  35870  funpartfun  35885  hftr  36124  itgeq12i  36148  filnetlem3  36323  bj-genr  36549  bj-genl  36550  bj-genan  36551  bj-mpgs  36552  bj-cbvalim  36588  bj-cbvexim  36589  bj-ax12v  36599  bj-ceqsalg0  36831  bj-ceqsalgALT  36833  bj-ceqsalgvALT  36835  bj-vtoclgfALT  37002  vtoclefex  37277  rdgeqoa  37313  exrecfnpw  37324  riscer  37935  trressn  38388  disjALTV0  38697  ax12eq  38884  cdleme32fva  40381  sbalexi  42192  unielss  43172  tfsconcatlem  43291  eu0  43475  dfrcl2  43629  rr-grothprim  44262  rr-grothshort  44266  pm11.11  44336  sbc3orgVD  44815  ordelordALTVD  44831  trsbcVD  44841  undif3VD  44846  sbcssgVD  44847  csbingVD  44848  onfrALTlem1VD  44854  onfrALTVD  44855  csbsngVD  44857  csbxpgVD  44858  csbresgVD  44859  csbrngVD  44860  csbima12gALTVD  44861  csbunigVD  44862  csbfv12gALTVD  44863  19.41rgVD  44866  unisnALT  44890  refsum2cnlem1  44930  dvnprodlem3  45861  sge00  46289  eusnsn  46933  aiota0def  47003  sprssspr  47363  spcdvw  48832  setrec2lem2  48847  onsetrec  48861
  Copyright terms: Public domain W3C validator