Axiom ax-gen 1722

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 32400 shows the special case ∀𝑥⊤. Theorem spi 2054 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 1481	1 wff ∀𝑥𝜑

This axiom is referenced by:  gen2  1723  mpg  1724  mpgbi  1725  mpgbir  1726  hbth  1729  stdpc6  1957  ax13dgen3  2016  cesare  2569  camestres  2570  calemes  2581  ceqsalg  3230  ceqsralv  3234  vtocl2  3261  mosub  3384  sbcth  3450  sbciegf  3467  csbiegf  3557  sbcnestg  3997  csbnestg  3998  csbnest1g  4001  int0OLD  4491  mpteq2ia  4740  mpteq2da  4743  ssopab2i  5003  relssi  5211  xpidtr  5518  funcnvsn  5936  caovmo  6871  ordom  7074  wfrfun  7425  tfrlem7  7479  pssnn  8178  findcard  8199  findcard2  8200  fiint  8237  inf0  8518  axinf2  8537  trcl  8604  axac3  9286  brdom3  9350  axpowndlem4  9422  axregndlem2  9425  axinfnd  9428  wfgru  9638  nqerf  9752  uzrdgfni  12757  ltweuz  12760  trclfvcotr  13750  fclim  14284  letsr  17227  distop  20799  fctop  20808  cctop  20810  ulmdm  24147  upgr0eopALT  26011  disjin  29399  disjin2  29400  bnj1023  30851  bnj1109  30857  bnj907  31035  hbimg  31715  frrlem5c  31786  fnsingle  32026  funimage  32035  funpartfun  32050  hftr  32289  filnetlem3  32375  allt  32400  alnof  32401  bj-genr  32591  bj-genl  32592  bj-genan  32593  bj-ax12  32634  bj-ceqsalg0  32877  bj-ceqsalgALT  32879  bj-ceqsalgvALT  32881  bj-vtoclgfALT  33021  vtoclefex  33181  rdgeqoa  33218  riscer  33787  ax12eq  34226  cdleme32fva  35725  dfrcl2  37966  pm11.11  38573  sbc3orgVD  39086  ordelordALTVD  39103  trsbcVD  39113  undif3VD  39118  sbcssgVD  39119  csbingVD  39120  onfrALTlem5VD  39121  onfrALTlem1VD  39126  onfrALTVD  39127  csbsngVD  39129  csbxpgVD  39130  csbresgVD  39131  csbrngVD  39132  csbima12gALTVD  39133  csbunigVD  39134  csbfv12gALTVD  39135  19.41rgVD  39138  unisnALT  39162  refsum2cnlem1  39196  mptssid  39450  dvnprodlem3  40163  sge00  40593  sprssspr  41731  spcdvw  42426  setrec2lem2  42441  onsetrec  42451