Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-gen GIF version

Axiom ax-gen 1425
 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 spi 1516 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, 5-Aug-1993.)
Hypothesis
Ref Expression
ax-g.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 1329 1 wff 𝑥𝜑
 Colors of variables: wff set class This axiom is referenced by:  gen2  1426  mpg  1427  mpgbi  1428  mpgbir  1429  hbth  1439  19.23h  1474  19.9ht  1620  stdpc6  1679  equveli  1732  cesare  2103  camestres  2104  calemes  2115  ceqsralv  2717  vtocl2  2741  euxfr2dc  2869  sbcth  2922  sbciegf  2940  csbiegf  3043  sbcnestg  3053  csbnestg  3054  csbnest1g  3055  int0  3785  mpteq2ia  4014  mpteq2da  4017  ssopab2i  4199  relssi  4630  xpidtr  4929  funcnvsn  5168  funinsn  5172  tfrlem7  6214  tfri1  6262  sucinc  6341  findcard  6782  findcard2  6783  findcard2s  6784  fiintim  6817  fisseneq  6820  frec2uzrand  10190  frec2uzf1od  10191  frecfzennn  10211  hashinfom  10536  zfz1iso  10596  fclim  11075  distop  12268  ch2var  13058  strcollnf  13267
 Copyright terms: Public domain W3C validator