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 2175 (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 1904). (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 1528 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  2028  sbt  2064  ax13dgen3  2136  ceqsalg  3534  ceqsralv  3538  vtocl2OLD  3567  mosub  3707  sbcth  3790  sbciegf  3812  csbiegf  3919  sbcnestgw  4375  csbnestgw  4376  sbcnestg  4380  csbnestg  4381  csbnest1g  4384  mpteq2ia  5153  mpteq2da  5156  al0ssb  5208  ssopab2i  5433  relssi  5658  xpidtr  5979  funcnvsn  6400  caovmo  7378  ordom  7580  wfrfun  7959  tfrlem7  8013  pssnn  8728  findcard  8749  findcard2  8750  fiint  8787  inf0  9076  axinf2  9095  trcl  9162  axac3  9878  brdom3  9942  axpowndlem4  10014  axregndlem2  10017  axinfnd  10020  wfgru  10230  nqerf  10344  uzrdgfni  13319  ltweuz  13322  trclfvcotr  14362  fclim  14903  letsr  17830  distop  21522  fctop  21531  cctop  21533  ulmdm  24899  upgr0eopALT  26818  bnj1023  31941  bnj1109  31947  bnj907  32126  funen1cnv  32244  loop1cycl  32271  umgr2cycl  32275  hbimg  32941  fnsingle  33267  funimage  33276  funpartfun  33291  hftr  33530  filnetlem3  33615  bj-genr  33827  bj-genl  33828  bj-genan  33829  bj-mpgs  33830  bj-cbvalim  33865  bj-cbvexim  33866  bj-ax12v  33876  bj-ceqsalg0  34091  bj-ceqsalgALT  34093  bj-ceqsalgvALT  34095  bj-vtoclgfALT  34236  vtoclefex  34487  rdgeqoa  34523  exrecfnpw  34534  riscer  35137  disjALTV0  35854  ax12eq  35947  cdleme32fva  37443  eu0  39754  dfrcl2  39887  rr-grothprim  40504  pm11.11  40574  sbc3orgVD  41053  ordelordALTVD  41069  trsbcVD  41079  undif3VD  41084  sbcssgVD  41085  csbingVD  41086  onfrALTlem1VD  41092  onfrALTVD  41093  csbsngVD  41095  csbxpgVD  41096  csbresgVD  41097  csbrngVD  41098  csbima12gALTVD  41099  csbunigVD  41100  csbfv12gALTVD  41101  19.41rgVD  41104  unisnALT  41128  refsum2cnlem1  41162  dvnprodlem3  42101  sge00  42527  eusnsn  43130  aiota0def  43163  sprssspr  43478  spcdvw  44617  setrec2lem2  44632  onsetrec  44645
 Copyright terms: Public domain W3C validator