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  2585  vtocl2  2609  euxfr2dc  2726  sbcth  2777  sbciegf  2794  csbiegf  2890  sbcnestg  2899  csbnestg  2900  csbnest1g  2901  int0  3629  mpteq2ia  3843  mpteq2da  3846  ssopab2i  4014  relssi  4431  xpidtr  4715  funcnvsn  4945  tfrlem7  5933  tfri1  5951  sucinc  6025  findcard  6345  findcard2  6346  findcard2s  6347  frec2uzzd  9160  frec2uzsucd  9161  frec2uzrand  9165  frec2uzf1od  9166  frecfzennn  9177  fclim  9789  ch2var  9881  strcollnf  10084
  Copyright terms: Public domain W3C validator