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 1797
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 1809 shows the special case 𝑥. The converse rule of inference spi 2177 (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 1913). (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 1539 1 wff 𝑥𝜑
Colors of variables: wff setvar class
This axiom is referenced by:  gen2  1798  mpg  1799  mpgbi  1800  mpgbir  1801  hbth  1805  altru  1809  alfal  1810  stdpc6  2031  sbt  2069  ax13dgen3  2135  ceqsalg  3507  ceqsralvOLD  3514  vtoclegft  3573  mosub  3709  sbcth  3792  sbciegf  3816  sbcg  3856  csbiegf  3927  sbcnestgw  4420  csbnestgw  4421  sbcnestg  4425  csbnestg  4426  csbnest1g  4429  mpteq2daOLD  5247  mpteq2iaOLD  5252  al0ssb  5308  intidg  5457  ssopab2i  5550  relssi  5787  xpidtr  6123  funcnvsn  6598  caovmo  7646  trom  7866  peano1  7881  abrexexg  7949  wfrfunOLD  8321  tfrlem7  8385  1onn  8641  2onn  8643  findcard  9165  findcard2  9166  pssnn  9170  ssfi  9175  pssnnOLD  9267  findcard2OLD  9286  fiint  9326  inf0  9618  axinf2  9637  trcl  9725  axac3  10461  brdom3  10525  axpowndlem4  10597  axregndlem2  10600  axinfnd  10603  wfgru  10813  nqerf  10927  uzrdgfni  13927  ltweuz  13930  trclfvcotr  14960  fclim  15501  letsr  18550  distop  22718  fctop  22727  cctop  22729  ulmdm  26129  upgr0eopALT  28631  bnj1023  34077  bnj1109  34083  bnj907  34264  funen1cnv  34377  loop1cycl  34414  umgr2cycl  34418  hbimg  35073  fnsingle  35183  funimage  35192  funpartfun  35207  hftr  35446  filnetlem3  35568  bj-genr  35787  bj-genl  35788  bj-genan  35789  bj-mpgs  35790  bj-cbvalim  35825  bj-cbvexim  35826  bj-ax12v  35836  bj-ceqsalg0  36071  bj-ceqsalgALT  36073  bj-ceqsalgvALT  36075  bj-vtoclgfALT  36243  vtoclefex  36518  rdgeqoa  36554  exrecfnpw  36565  riscer  37159  trressn  37618  disjALTV0  37927  ax12eq  38114  cdleme32fva  39611  unielss  42269  tfsconcatlem  42388  eu0  42573  dfrcl2  42727  rr-grothprim  43361  rr-grothshort  43365  pm11.11  43435  sbc3orgVD  43914  ordelordALTVD  43930  trsbcVD  43940  undif3VD  43945  sbcssgVD  43946  csbingVD  43947  onfrALTlem1VD  43953  onfrALTVD  43954  csbsngVD  43956  csbxpgVD  43957  csbresgVD  43958  csbrngVD  43959  csbima12gALTVD  43960  csbunigVD  43961  csbfv12gALTVD  43962  19.41rgVD  43965  unisnALT  43989  refsum2cnlem1  44023  dvnprodlem3  44963  sge00  45391  eusnsn  46035  aiota0def  46103  sprssspr  46448  spcdvw  47812  setrec2lem2  47827  onsetrec  47841
  Copyright terms: Public domain W3C validator