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 1798
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 1810 shows the special case 𝑥. The converse rule of inference spi 2178 (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 1914). (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  1799  mpg  1800  mpgbi  1801  mpgbir  1802  hbth  1806  altru  1810  alfal  1811  stdpc6  2032  sbt  2070  ax13dgen3  2136  ceqsalg  3508  ceqsralvOLD  3515  vtoclegft  3574  mosub  3710  sbcth  3793  sbciegf  3817  sbcg  3857  csbiegf  3928  sbcnestgw  4421  csbnestgw  4422  sbcnestg  4426  csbnestg  4427  csbnest1g  4430  mpteq2daOLD  5248  mpteq2iaOLD  5253  al0ssb  5309  intidg  5458  ssopab2i  5551  relssi  5788  xpidtr  6124  funcnvsn  6599  caovmo  7644  trom  7864  peano1  7879  abrexexg  7947  wfrfunOLD  8319  tfrlem7  8383  1onn  8639  2onn  8641  findcard  9163  findcard2  9164  pssnn  9168  ssfi  9173  pssnnOLD  9265  findcard2OLD  9284  fiint  9324  inf0  9616  axinf2  9635  trcl  9723  axac3  10459  brdom3  10523  axpowndlem4  10595  axregndlem2  10598  axinfnd  10601  wfgru  10811  nqerf  10925  uzrdgfni  13923  ltweuz  13926  trclfvcotr  14956  fclim  15497  letsr  18546  distop  22498  fctop  22507  cctop  22509  ulmdm  25905  upgr0eopALT  28376  bnj1023  33791  bnj1109  33797  bnj907  33978  funen1cnv  34091  loop1cycl  34128  umgr2cycl  34132  hbimg  34781  fnsingle  34891  funimage  34900  funpartfun  34915  hftr  35154  filnetlem3  35265  bj-genr  35484  bj-genl  35485  bj-genan  35486  bj-mpgs  35487  bj-cbvalim  35522  bj-cbvexim  35523  bj-ax12v  35533  bj-ceqsalg0  35768  bj-ceqsalgALT  35770  bj-ceqsalgvALT  35772  bj-vtoclgfALT  35940  vtoclefex  36215  rdgeqoa  36251  exrecfnpw  36262  riscer  36856  trressn  37315  disjALTV0  37624  ax12eq  37811  cdleme32fva  39308  unielss  41967  tfsconcatlem  42086  eu0  42271  dfrcl2  42425  rr-grothprim  43059  rr-grothshort  43063  pm11.11  43133  sbc3orgVD  43612  ordelordALTVD  43628  trsbcVD  43638  undif3VD  43643  sbcssgVD  43644  csbingVD  43645  onfrALTlem1VD  43651  onfrALTVD  43652  csbsngVD  43654  csbxpgVD  43655  csbresgVD  43656  csbrngVD  43657  csbima12gALTVD  43658  csbunigVD  43659  csbfv12gALTVD  43660  19.41rgVD  43663  unisnALT  43687  refsum2cnlem1  43721  dvnprodlem3  44664  sge00  45092  eusnsn  45736  aiota0def  45804  sprssspr  46149  spcdvw  47724  setrec2lem2  47739  onsetrec  47753
  Copyright terms: Public domain W3C validator