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 1859
Description: Rule of Generalization. The postulated inference rule of predicate 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 𝑥 = 𝑥, we can conclude 𝑥𝑥 = 𝑥 or even 𝑦𝑥 = 𝑥. Theorem allt 32677 shows the special case 𝑥. Theorem spi 2189 shows we can go the other way also: in other words we can add or remove universal quantifiers from the beginning of any theorem as required. (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 1618 1 wff 𝑥𝜑
Colors of variables: wff setvar class
This axiom is referenced by:  gen2  1860  mpg  1861  mpgbi  1862  mpgbir  1863  hbth  1866  stdpc6  2098  ax13dgen3  2153  cesare  2695  camestres  2696  calemes  2707  ceqsalg  3358  ceqsralv  3362  vtocl2  3389  mosub  3513  sbcth  3579  sbciegf  3596  csbiegf  3686  sbcnestg  4128  csbnestg  4129  csbnest1g  4132  int0OLD  4631  mpteq2ia  4880  mpteq2da  4883  ssopab2i  5141  relssi  5356  xpidtr  5664  funcnvsn  6085  caovmo  7024  ordom  7227  wfrfun  7582  tfrlem7  7636  pssnn  8331  findcard  8352  findcard2  8353  fiint  8390  inf0  8679  axinf2  8698  trcl  8765  axac3  9449  brdom3  9513  axpowndlem4  9585  axregndlem2  9588  axinfnd  9591  wfgru  9801  nqerf  9915  uzrdgfni  12922  ltweuz  12925  trclfvcotr  13920  fclim  14454  letsr  17399  distop  20972  fctop  20981  cctop  20983  ulmdm  24317  upgr0eopALT  26181  disjin  29677  disjin2  29678  bnj1023  31129  bnj1109  31135  bnj907  31313  hbimg  31991  frrlem5c  32063  fnsingle  32303  funimage  32312  funpartfun  32327  hftr  32566  filnetlem3  32652  allt  32677  alnof  32678  bj-genr  32868  bj-genl  32869  bj-genan  32870  bj-ax12  32911  bj-ceqsalg0  33154  bj-ceqsalgALT  33156  bj-ceqsalgvALT  33158  bj-vtoclgfALT  33298  vtoclefex  33463  rdgeqoa  33500  riscer  34069  ax12eq  34699  cdleme32fva  36196  dfrcl2  38437  pm11.11  39044  sbc3orgVD  39554  ordelordALTVD  39571  trsbcVD  39581  undif3VD  39586  sbcssgVD  39587  csbingVD  39588  onfrALTlem1VD  39594  onfrALTVD  39595  csbsngVD  39597  csbxpgVD  39598  csbresgVD  39599  csbrngVD  39600  csbima12gALTVD  39601  csbunigVD  39602  csbfv12gALTVD  39603  19.41rgVD  39606  unisnALT  39630  refsum2cnlem1  39664  mptssid  39918  dvnprodlem3  40635  sge00  41065  sprssspr  42210  spcdvw  42905  setrec2lem2  42920  onsetrec  42933
  Copyright terms: Public domain W3C validator