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 1789
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 1801 shows the special case 𝑥. The converse rule of inference spi 2169 (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 1905). (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 1531 1 wff 𝑥𝜑
Colors of variables: wff setvar class
This axiom is referenced by:  gen2  1790  mpg  1791  mpgbi  1792  mpgbir  1793  hbth  1797  altru  1801  alfal  1802  stdpc6  2023  sbt  2061  ax13dgen3  2127  ceqsalg  3500  ceqsralvOLD  3507  vtoclegft  3566  mosub  3702  sbcth  3785  sbciegf  3809  sbcg  3849  csbiegf  3920  sbcnestgw  4413  csbnestgw  4414  sbcnestg  4418  csbnestg  4419  csbnest1g  4422  mpteq2daOLD  5238  mpteq2iaOLD  5243  al0ssb  5299  intidg  5448  ssopab2i  5541  relssi  5778  xpidtr  6114  funcnvsn  6589  caovmo  7638  trom  7858  peano1  7873  abrexexg  7941  wfrfunOLD  8315  tfrlem7  8379  1onn  8636  2onn  8638  findcard  9160  findcard2  9161  pssnn  9165  ssfi  9170  pssnnOLD  9262  findcard2OLD  9281  fiint  9321  inf0  9613  axinf2  9632  trcl  9720  axac3  10456  brdom3  10520  axpowndlem4  10592  axregndlem2  10595  axinfnd  10598  wfgru  10808  nqerf  10922  uzrdgfni  13921  ltweuz  13924  trclfvcotr  14954  fclim  15495  letsr  18550  distop  22822  fctop  22831  cctop  22833  ulmdm  26248  upgr0eopALT  28848  bnj1023  34282  bnj1109  34288  bnj907  34469  funen1cnv  34582  loop1cycl  34619  umgr2cycl  34623  hbimg  35277  fnsingle  35387  funimage  35396  funpartfun  35411  hftr  35650  filnetlem3  35756  bj-genr  35975  bj-genl  35976  bj-genan  35977  bj-mpgs  35978  bj-cbvalim  36013  bj-cbvexim  36014  bj-ax12v  36024  bj-ceqsalg0  36259  bj-ceqsalgALT  36261  bj-ceqsalgvALT  36263  bj-vtoclgfALT  36431  vtoclefex  36706  rdgeqoa  36742  exrecfnpw  36753  riscer  37350  trressn  37809  disjALTV0  38118  ax12eq  38305  cdleme32fva  39802  unielss  42481  tfsconcatlem  42600  eu0  42785  dfrcl2  42939  rr-grothprim  43573  rr-grothshort  43577  pm11.11  43647  sbc3orgVD  44126  ordelordALTVD  44142  trsbcVD  44152  undif3VD  44157  sbcssgVD  44158  csbingVD  44159  onfrALTlem1VD  44165  onfrALTVD  44166  csbsngVD  44168  csbxpgVD  44169  csbresgVD  44170  csbrngVD  44171  csbima12gALTVD  44172  csbunigVD  44173  csbfv12gALTVD  44174  19.41rgVD  44177  unisnALT  44201  refsum2cnlem1  44235  dvnprodlem3  45174  sge00  45602  eusnsn  46246  aiota0def  46314  sprssspr  46659  spcdvw  47936  setrec2lem2  47951  onsetrec  47965
  Copyright terms: Public domain W3C validator