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 1802
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 1814 shows the special case 𝑥. The converse rule of inference spi 2185 (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 1917). (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 1540 1 wff 𝑥𝜑
Colors of variables: wff setvar class
This axiom is referenced by:  gen2  1803  mpg  1804  mpgbi  1805  mpgbir  1806  hbth  1810  altru  1814  alfal  1815  stdpc6  2040  sbt  2076  ax13dgen3  2143  ceqsalg  3430  ceqsralvOLD  3436  mosub  3612  sbcth  3695  sbciegf  3719  csbiegf  3823  sbcnestgw  4310  csbnestgw  4311  sbcnestg  4315  csbnestg  4316  csbnest1g  4319  mpteq2ia  5121  mpteq2da  5124  al0ssb  5176  ssopab2i  5405  relssi  5631  xpidtr  5956  funcnvsn  6389  caovmo  7401  ordom  7608  wfrfun  7994  tfrlem7  8048  findcard  8762  findcard2  8763  pssnn  8767  ssfi  8772  pssnnOLD  8815  findcard2OLD  8834  fiint  8869  inf0  9157  axinf2  9176  trcl  9243  axac3  9964  brdom3  10028  axpowndlem4  10100  axregndlem2  10103  axinfnd  10106  wfgru  10316  nqerf  10430  uzrdgfni  13417  ltweuz  13420  trclfvcotr  14458  fclim  15000  letsr  17953  distop  21746  fctop  21755  cctop  21757  ulmdm  25140  upgr0eopALT  27061  bnj1023  32331  bnj1109  32337  bnj907  32518  funen1cnv  32631  loop1cycl  32670  umgr2cycl  32674  hbimg  33357  fnsingle  33859  funimage  33868  funpartfun  33883  hftr  34122  filnetlem3  34207  bj-genr  34426  bj-genl  34427  bj-genan  34428  bj-mpgs  34429  bj-cbvalim  34464  bj-cbvexim  34465  bj-ax12v  34475  bj-ceqsalg0  34705  bj-ceqsalgALT  34707  bj-ceqsalgvALT  34709  bj-vtoclgfALT  34853  vtoclefex  35128  rdgeqoa  35164  exrecfnpw  35175  riscer  35769  disjALTV0  36485  ax12eq  36578  cdleme32fva  38074  eu0  40681  dfrcl2  40828  rr-grothprim  41460  pm11.11  41530  sbc3orgVD  42009  ordelordALTVD  42025  trsbcVD  42035  undif3VD  42040  sbcssgVD  42041  csbingVD  42042  onfrALTlem1VD  42048  onfrALTVD  42049  csbsngVD  42051  csbxpgVD  42052  csbresgVD  42053  csbrngVD  42054  csbima12gALTVD  42055  csbunigVD  42056  csbfv12gALTVD  42057  19.41rgVD  42060  unisnALT  42084  refsum2cnlem1  42118  dvnprodlem3  43031  sge00  43456  eusnsn  44059  aiota0def  44120  sprssspr  44467  spcdvw  45838  setrec2lem2  45853  onsetrec  45866
  Copyright terms: Public domain W3C validator