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 1719
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 32039 shows the special case 𝑥. Theorem spi 2052 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 1478 1 wff 𝑥𝜑
Colors of variables: wff setvar class
This axiom is referenced by:  gen2  1720  mpg  1721  mpgbi  1722  mpgbir  1723  hbth  1726  stdpc6  1954  ax13dgen3  2013  cesare  2568  camestres  2569  calemes  2580  ceqsalg  3216  ceqsralv  3220  vtocl2  3247  mosub  3366  sbcth  3432  sbciegf  3449  csbiegf  3538  sbcnestg  3969  csbnestg  3970  csbnest1g  3973  int0OLD  4456  mpteq2ia  4700  mpteq2da  4703  ssopab2i  4963  relssi  5172  xpidtr  5477  funcnvsn  5894  caovmo  6824  ordom  7021  wfrfun  7370  tfrlem7  7424  pssnn  8122  findcard  8143  findcard2  8144  fiint  8181  inf0  8462  axinf2  8481  trcl  8548  axac3  9230  brdom3  9294  axpowndlem4  9366  axregndlem2  9369  axinfnd  9372  wfgru  9582  nqerf  9696  uzrdgfni  12697  ltweuz  12700  trclfvcotr  13684  fclim  14218  letsr  17148  distop  20710  fctop  20718  cctop  20720  ulmdm  24051  upgr0eopALT  25906  disjin  29241  disjin2  29242  bnj1023  30556  bnj1109  30562  bnj907  30740  hbimg  31413  frrlem5c  31484  fnsingle  31665  funimage  31674  funpartfun  31689  hftr  31928  filnetlem3  32014  allt  32039  alnof  32040  bj-genr  32230  bj-genl  32231  bj-genan  32232  bj-ax12  32273  bj-ceqsalg0  32521  bj-ceqsalgALT  32523  bj-ceqsalgvALT  32525  bj-vtoclgfALT  32665  vtoclefex  32810  rdgeqoa  32847  riscer  33416  ax12eq  33703  cdleme32fva  35202  dfrcl2  37444  pm11.11  38052  sbc3orgVD  38566  ordelordALTVD  38583  trsbcVD  38593  undif3VD  38598  sbcssgVD  38599  csbingVD  38600  onfrALTlem5VD  38601  onfrALTlem1VD  38606  onfrALTVD  38607  csbsngVD  38609  csbxpgVD  38610  csbresgVD  38611  csbrngVD  38612  csbima12gALTVD  38613  csbunigVD  38614  csbfv12gALTVD  38615  19.41rgVD  38618  unisnALT  38642  refsum2cnlem1  38676  mptssid  38922  dvnprodlem3  39466  sge00  39897  sprssspr  41016  spcdvw  41715  setrec2lem2  41731  onsetrec  41741
  Copyright terms: Public domain W3C validator