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

Axiom ax-gen 1338
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 1429 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 1241 1 wff 𝑥𝜑
Colors of variables: wff set class
This axiom is referenced by:  gen2  1339  mpg  1340  mpgbi  1341  mpgbir  1342  hbth  1352  19.23h  1387  19.9ht  1532  stdpc6  1591  equveli  1642  cesare  2004  camestres  2005  calemes  2016  ceqsralv  2582  vtocl2  2606  euxfr2dc  2723  sbcth  2774  sbciegf  2791  csbiegf  2887  sbcnestg  2896  csbnestg  2897  csbnest1g  2898  int0  3626  mpteq2ia  3840  mpteq2da  3843  ssopab2i  4011  relssi  4394  xpidtr  4678  funcnvsn  4908  tfrlem7  5896  tfri1  5914  sucinc  5988  findcard  6307  findcard2  6308  findcard2s  6309  frec2uzzd  9040  frec2uzsucd  9041  frec2uzrand  9045  frec2uzf1od  9046  frecfzennn  9057  fclim  9668  ch2var  9756  strcollnf  9959
  Copyright terms: Public domain W3C validator