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 1870
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 32736 shows the special case 𝑥. Theorem spi 2208 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 1629 1 wff 𝑥𝜑
Colors of variables: wff setvar class
This axiom is referenced by:  gen2  1871  mpg  1872  mpgbi  1873  mpgbir  1874  hbth  1877  stdpc6  2113  ax13dgen3  2171  cesare  2718  camestres  2719  calemes  2730  ceqsalg  3382  ceqsralv  3386  vtocl2  3412  mosub  3536  sbcth  3602  sbciegf  3619  csbiegf  3706  sbcnestg  4142  csbnestg  4143  csbnest1g  4146  mpteq2ia  4875  mpteq2da  4878  ssopab2i  5137  relssi  5350  xpidtr  5658  funcnvsn  6078  caovmo  7021  ordom  7224  wfrfun  7581  tfrlem7  7635  pssnn  8337  findcard  8358  findcard2  8359  fiint  8396  inf0  8685  axinf2  8704  trcl  8771  axac3  9491  brdom3  9555  axpowndlem4  9627  axregndlem2  9630  axinfnd  9633  wfgru  9843  nqerf  9957  uzrdgfni  12964  ltweuz  12967  trclfvcotr  13957  fclim  14491  letsr  17434  distop  21019  fctop  21028  cctop  21030  ulmdm  24366  upgr0eopALT  26231  disjin  29736  disjin2  29737  bnj1023  31188  bnj1109  31194  bnj907  31372  hbimg  32050  frrlem5c  32122  fnsingle  32362  funimage  32371  funpartfun  32386  hftr  32625  filnetlem3  32711  allt  32736  alnof  32737  bj-genr  32927  bj-genl  32928  bj-genan  32929  bj-ax12  32971  bj-ceqsalg0  33205  bj-ceqsalgALT  33207  bj-ceqsalgvALT  33209  bj-vtoclgfALT  33351  vtoclefex  33517  rdgeqoa  33554  riscer  34118  ax12eq  34748  cdleme32fva  36246  dfrcl2  38492  pm11.11  39099  sbc3orgVD  39608  ordelordALTVD  39625  trsbcVD  39635  undif3VD  39640  sbcssgVD  39641  csbingVD  39642  onfrALTlem1VD  39648  onfrALTVD  39649  csbsngVD  39651  csbxpgVD  39652  csbresgVD  39653  csbrngVD  39654  csbima12gALTVD  39655  csbunigVD  39656  csbfv12gALTVD  39657  19.41rgVD  39660  unisnALT  39684  refsum2cnlem1  39718  mptssid  39965  dvnprodlem3  40678  sge00  41107  sprssspr  42256  spcdvw  42951  setrec2lem2  42966  onsetrec  42979
  Copyright terms: Public domain W3C validator