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 1894
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 1906 shows the special case 𝑥. The converse rule of inference spi 2225 (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 2009). (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 1654 1 wff 𝑥𝜑
Colors of variables: wff setvar class
This axiom is referenced by:  gen2  1895  mpg  1896  mpgbi  1897  mpgbir  1898  hbth  1902  altru  1906  alfal  1907  stdpc6  2132  ax13dgen3  2190  cesareOLD  2756  camestresOLD  2758  calemesOLD  2777  ceqsalg  3447  ceqsralv  3451  vtocl2  3477  mosub  3609  sbcth  3677  sbciegf  3694  csbiegf  3781  sbcnestg  4223  csbnestg  4224  csbnest1g  4227  mpteq2ia  4965  mpteq2da  4968  al0ssb  5017  ssopab2i  5231  relssi  5449  xpidtr  5764  funcnvsn  6176  caovmo  7136  ordom  7340  wfrfun  7696  tfrlem7  7750  pssnn  8453  findcard  8474  findcard2  8475  fiint  8512  inf0  8802  axinf2  8821  trcl  8888  axac3  9608  brdom3  9672  axpowndlem4  9744  axregndlem2  9747  axinfnd  9750  wfgru  9960  nqerf  10074  uzrdgfni  13059  ltweuz  13062  trclfvcotr  14134  fclim  14668  letsr  17587  distop  21177  fctop  21186  cctop  21188  ulmdm  24553  upgr0eopALT  26421  disjin  29942  disjin2  29943  bnj1023  31393  bnj1109  31399  bnj907  31577  hbimg  32248  frrlem5c  32320  fnsingle  32560  funimage  32569  funpartfun  32584  hftr  32823  filnetlem3  32908  bj-genr  33115  bj-genl  33116  bj-genan  33117  bj-cbvalim  33145  bj-cbvexim  33146  bj-ax12  33170  bj-ceqsalg0  33396  bj-ceqsalgALT  33398  bj-ceqsalgvALT  33400  bj-vtoclgfALT  33542  vtoclefex  33726  rdgeqoa  33762  riscer  34328  ax12eq  35015  cdleme32fva  36511  dfrcl2  38806  pm11.11  39412  sbc3orgVD  39904  ordelordALTVD  39920  trsbcVD  39930  undif3VD  39935  sbcssgVD  39936  csbingVD  39937  onfrALTlem1VD  39943  onfrALTVD  39944  csbsngVD  39946  csbxpgVD  39947  csbresgVD  39948  csbrngVD  39949  csbima12gALTVD  39950  csbunigVD  39951  csbfv12gALTVD  39952  19.41rgVD  39955  unisnALT  39979  refsum2cnlem1  40013  mptssid  40249  dvnprodlem3  40956  sge00  41382  eusnsn  41960  aiota0def  41989  sprssspr  42596  spcdvw  43335  setrec2lem2  43350  onsetrec  43363
  Copyright terms: Public domain W3C validator