Axiom ax-gen 1713

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 31570 shows the special case ∀𝑥⊤. Theorem spi 2042 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

Step	Hyp	Ref	Expression
1		wph	. 2 wff 𝜑
2		vx	. 2 setvar 𝑥
3	1, 2	wal 1473	1 wff ∀𝑥𝜑

This axiom is referenced by:  gen2  1714  mpg  1715  mpgbi  1716  mpgbir  1717  hbth  1720  stdpc6  1944  ax13dgen3  2003  cesare  2557  camestres  2558  calemes  2569  ceqsalg  3203  ceqsralv  3207  vtocl2  3234  mosub  3351  sbcth  3417  sbciegf  3434  csbiegf  3523  sbcnestg  3949  csbnestg  3950  csbnest1g  3953  int0OLD  4426  mpteq2ia  4668  mpteq2da  4671  ssopab2i  4928  relssi  5134  xpidtr  5437  funcnvsn  5850  caovmo  6769  ordom  6966  wfrfun  7312  tfrlem7  7366  pssnn  8063  findcard  8084  findcard2  8085  fiint  8122  inf0  8401  axinf2  8420  trcl  8487  axac3  9169  brdom3  9231  axpowndlem4  9301  axregndlem2  9304  axinfnd  9307  wfgru  9517  nqerf  9631  uzrdgfni  12619  ltweuz  12622  trclfvcotr  13598  fclim  14132  letsr  17050  distop  20610  fctop  20618  cctop  20620  ulmdm  23951  upgr0eopALT  25782  0egra0rgra  26463  disjin  28781  disjin2  28782  bnj1023  30105  bnj1109  30111  bnj907  30289  hbimg  30959  frrlem5c  31030  fnsingle  31196  funimage  31205  funpartfun  31220  hftr  31459  filnetlem3  31545  allt  31570  alnof  31571  bj-genr  31776  bj-genl  31777  bj-genan  31778  bj-ax12  31823  bj-ceqsalg0  32071  bj-ceqsalgALT  32073  bj-ceqsalgvALT  32075  bj-vtoclgfALT  32212  vtoclefex  32357  rdgeqoa  32394  riscer  32957  ax12eq  33244  cdleme32fva  34743  dfrcl2  36985  pm11.11  37595  sbc3orgVD  38108  ordelordALTVD  38125  trsbcVD  38135  undif3VD  38140  sbcssgVD  38141  csbingVD  38142  onfrALTlem5VD  38143  onfrALTlem1VD  38148  onfrALTVD  38149  csbsngVD  38151  csbxpgVD  38152  csbresgVD  38153  csbrngVD  38154  csbima12gALTVD  38155  csbunigVD  38156  csbfv12gALTVD  38157  19.41rgVD  38160  unisnALT  38184  refsum2cnlem1  38219  dvnprodlem3  38838  sge00  39269  spcdvw  42224  setrec2lem2  42240  onsetrec  42250