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 1795
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 1807 shows the special case 𝑥. The converse rule of inference spi 2184 (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 1910). (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 1538 1 wff 𝑥𝜑
Colors of variables: wff setvar class
This axiom is referenced by:  gen2  1796  mpg  1797  mpgbi  1798  mpgbir  1799  hbth  1803  altru  1807  alfal  1808  stdpc6  2027  sbt  2066  ax13dgen3  2139  ceqsalg  3516  vtoclegft  3587  mosub  3718  sbcth  3802  sbciegf  3826  sbcg  3862  csbiegf  3931  sbcnestgw  4422  csbnestgw  4423  sbcnestg  4427  csbnestg  4428  csbnest1g  4431  mpteq2daOLD  5239  mpteq2iaOLD  5244  al0ssb  5306  intidg  5460  ssopab2i  5553  relssi  5795  xpidtr  6140  funcnvsn  6614  caovmo  7667  trom  7892  peano1  7906  abrexexg  7981  wfrfunOLD  8355  tfrlem7  8419  1onn  8674  2onn  8676  findcard  9199  findcard2  9200  pssnn  9204  ssfi  9209  fiint  9362  fiintOLD  9363  inf0  9657  axinf2  9676  trcl  9764  axac3  10500  brdom3  10564  axpowndlem4  10636  axregndlem2  10639  axinfnd  10642  wfgru  10852  nqerf  10966  uzrdgfni  13995  ltweuz  13998  trclfvcotr  15044  fclim  15585  letsr  18634  cnsubrglem  21426  distop  22992  fctop  23001  cctop  23003  ulmdm  26426  upgr0eopALT  29123  bnj1023  34772  bnj1109  34778  bnj907  34959  funen1cnv  35080  axnulg  35084  loop1cycl  35120  umgr2cycl  35124  hbimg  35788  fnsingle  35898  funimage  35907  funpartfun  35922  hftr  36161  itgeq12i  36185  filnetlem3  36359  bj-genr  36585  bj-genl  36586  bj-genan  36587  bj-mpgs  36588  bj-cbvalim  36624  bj-cbvexim  36625  bj-ax12v  36635  bj-ceqsalg0  36867  bj-ceqsalgALT  36869  bj-ceqsalgvALT  36871  bj-vtoclgfALT  37038  vtoclefex  37313  rdgeqoa  37349  exrecfnpw  37360  riscer  37973  trressn  38424  disjALTV0  38733  ax12eq  38920  cdleme32fva  40417  sbalexi  42230  unielss  43208  tfsconcatlem  43327  eu0  43511  dfrcl2  43665  rr-grothprim  44297  rr-grothshort  44301  pm11.11  44371  sbc3orgVD  44849  ordelordALTVD  44865  trsbcVD  44875  undif3VD  44880  sbcssgVD  44881  csbingVD  44882  onfrALTlem1VD  44888  onfrALTVD  44889  csbsngVD  44891  csbxpgVD  44892  csbresgVD  44893  csbrngVD  44894  csbima12gALTVD  44895  csbunigVD  44896  csbfv12gALTVD  44897  19.41rgVD  44900  unisnALT  44924  wfaxrep  44984  refsum2cnlem1  45015  dvnprodlem3  45936  sge00  46364  eusnsn  47011  aiota0def  47081  sprssspr  47441  spcdvw  49171  setrec2lem2  49186  onsetrec  49200
  Copyright terms: Public domain W3C validator