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 1787
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 1799 shows the special case 𝑥. The converse rule of inference spi 2173 (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 1902). (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 1526 1 wff 𝑥𝜑
Colors of variables: wff setvar class
This axiom is referenced by:  gen2  1788  mpg  1789  mpgbi  1790  mpgbir  1791  hbth  1795  altru  1799  alfal  1800  stdpc6  2026  sbt  2062  ax13dgen3  2134  ceqsalg  3530  ceqsralv  3534  vtocl2OLD  3563  mosub  3703  sbcth  3786  sbciegf  3808  csbiegf  3915  sbcnestgw  4371  csbnestgw  4372  sbcnestg  4376  csbnestg  4377  csbnest1g  4380  mpteq2ia  5149  mpteq2da  5152  al0ssb  5204  ssopab2i  5429  relssi  5654  xpidtr  5976  funcnvsn  6398  caovmo  7374  ordom  7577  wfrfun  7956  tfrlem7  8010  pssnn  8725  findcard  8746  findcard2  8747  fiint  8784  inf0  9073  axinf2  9092  trcl  9159  axac3  9875  brdom3  9939  axpowndlem4  10011  axregndlem2  10014  axinfnd  10017  wfgru  10227  nqerf  10341  uzrdgfni  13316  ltweuz  13319  trclfvcotr  14359  fclim  14900  letsr  17827  distop  21533  fctop  21542  cctop  21544  ulmdm  24910  upgr0eopALT  26829  bnj1023  31952  bnj1109  31958  bnj907  32137  funen1cnv  32255  loop1cycl  32282  umgr2cycl  32286  hbimg  32952  fnsingle  33278  funimage  33287  funpartfun  33302  hftr  33541  filnetlem3  33626  bj-genr  33838  bj-genl  33839  bj-genan  33840  bj-mpgs  33841  bj-cbvalim  33876  bj-cbvexim  33877  bj-ax12v  33887  bj-ceqsalg0  34102  bj-ceqsalgALT  34104  bj-ceqsalgvALT  34106  bj-vtoclgfALT  34247  vtoclefex  34498  rdgeqoa  34534  exrecfnpw  34545  riscer  35149  disjALTV0  35866  ax12eq  35959  cdleme32fva  37455  eu0  39766  dfrcl2  39899  rr-grothprim  40516  pm11.11  40586  sbc3orgVD  41065  ordelordALTVD  41081  trsbcVD  41091  undif3VD  41096  sbcssgVD  41097  csbingVD  41098  onfrALTlem1VD  41104  onfrALTVD  41105  csbsngVD  41107  csbxpgVD  41108  csbresgVD  41109  csbrngVD  41110  csbima12gALTVD  41111  csbunigVD  41112  csbfv12gALTVD  41113  19.41rgVD  41116  unisnALT  41140  refsum2cnlem1  41174  dvnprodlem3  42113  sge00  42539  eusnsn  43142  aiota0def  43175  sprssspr  43490  spcdvw  44680  setrec2lem2  44695  onsetrec  44708
  Copyright terms: Public domain W3C validator