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 1712
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 31376 shows the special case 𝑥. Theorem spi 2041 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 1472 1 wff 𝑥𝜑
Colors of variables: wff setvar class
This axiom is referenced by:  gen2  1713  mpg  1714  mpgbi  1715  mpgbir  1716  hbth  1719  stdpc6  1943  ax13dgen3  2002  cesare  2556  camestres  2557  calemes  2568  ceqsalg  3202  ceqsralv  3206  vtocl2  3233  mosub  3350  sbcth  3416  sbciegf  3433  csbiegf  3522  sbcnestg  3948  csbnestg  3949  csbnest1g  3952  int0OLD  4420  mpteq2ia  4662  mpteq2da  4665  ssopab2i  4918  relssi  5123  xpidtr  5424  funcnvsn  5836  caovmo  6746  ordom  6943  wfrfun  7289  tfrlem7  7343  pssnn  8040  findcard  8061  findcard2  8062  fiint  8099  inf0  8378  axinf2  8397  trcl  8464  axac3  9146  brdom3  9208  axpowndlem4  9278  axregndlem2  9281  axinfnd  9284  wfgru  9494  nqerf  9608  uzrdgfni  12574  ltweuz  12577  trclfvcotr  13544  fclim  14078  letsr  16996  distop  20552  fctop  20560  cctop  20562  ulmdm  23868  0egra0rgra  26229  disjin  28587  disjin2  28588  bnj1023  29911  bnj1109  29917  bnj907  30095  hbimg  30765  frrlem5c  30836  fnsingle  31002  funimage  31011  funpartfun  31026  hftr  31265  filnetlem3  31351  allt  31376  alnof  31377  bj-genr  31582  bj-genl  31583  bj-genan  31584  bj-ax12  31629  bj-ceqsalg0  31867  bj-ceqsalgALT  31869  bj-ceqsalgvALT  31871  bj-vtoclgfALT  32008  vtoclefex  32153  rdgeqoa  32190  riscer  32753  ax12eq  33040  cdleme32fva  34539  dfrcl2  36781  pm11.11  37391  sbc3orgVD  37904  ordelordALTVD  37921  trsbcVD  37931  undif3VD  37936  sbcssgVD  37937  csbingVD  37938  onfrALTlem5VD  37939  onfrALTlem1VD  37944  onfrALTVD  37945  csbsngVD  37947  csbxpgVD  37948  csbresgVD  37949  csbrngVD  37950  csbima12gALTVD  37951  csbunigVD  37952  csbfv12gALTVD  37953  19.41rgVD  37956  unisnALT  37980  refsum2cnlem1  38015  dvnprodlem3  38635  sge00  39066  upgr0eopALT  40336
  Copyright terms: Public domain W3C validator