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 1698
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 31210 shows the special case 𝑥. Theorem spi 1995 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 1466 1 wff 𝑥𝜑
Colors of variables: wff setvar class
This axiom is referenced by:  gen2  1699  mpg  1700  mpgbi  1701  mpgbir  1702  hbth  1704  stdpc6  1906  ax13dgen3  1963  cesare  2452  camestres  2453  calemes  2464  ceqsalg  3093  ceqsralv  3097  vtocl2  3123  mosub  3240  sbcth  3306  sbciegf  3323  csbiegf  3409  sbcnestg  3826  csbnestg  3827  csbnest1g  3830  int0  4278  mpteq2ia  4518  mpteq2da  4521  ssopab2i  4770  relssi  4973  xpidtr  5272  funcnvsn  5679  caovmo  6581  ordom  6778  wfrfun  7123  tfrlem7  7178  pssnn  7874  findcard  7895  findcard2  7896  fiint  7933  inf0  8211  axinf2  8230  trcl  8297  axac3  8979  brdom3  9041  axpowndlem4  9110  axregndlem2  9113  axinfnd  9116  wfgru  9326  nqerf  9440  uzrdgfni  12285  ltweuz  12288  trclfvcotr  13233  fclim  13777  letsr  16638  distop  20168  fctop  20176  cctop  20178  ulmdm  23509  0egra0rgra  25824  disjin  28355  disjin2  28356  bnj1023  29744  bnj1109  29750  bnj907  29928  hbimg  30607  frrlem5c  30671  fnsingle  30837  funimage  30846  funpartfun  30861  hftr  31100  filnetlem3  31185  allt  31210  alnof  31211  bj-ax12  31429  bj-ceqsalg0  31670  bj-ceqsalgALT  31672  bj-ceqsalgvALT  31674  bj-vtoclgfALT  31811  vtoclefex  31957  rdgeqoa  31994  riscer  32464  ax12eq  32745  cdleme32fva  34244  dfrcl2  36505  pm11.11  37080  sbc3orgVD  37595  ordelordALTVD  37612  trsbcVD  37622  undif3VD  37627  sbcssgVD  37628  csbingVD  37629  onfrALTlem5VD  37630  onfrALTlem1VD  37635  onfrALTVD  37636  csbsngVD  37638  csbxpgVD  37639  csbresgVD  37640  csbrngVD  37641  csbima12gALTVD  37642  csbunigVD  37643  csbfv12gALTVD  37644  19.41rgVD  37647  unisnALT  37671  refsum2cnlem1  37706  dvnprodlem3  38242  sge00  38664  upgr0eopALT  39741
  Copyright terms: Public domain W3C validator