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

Axiom ax-gen 1314
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 1407 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
2 vx . 2  setvar
31, 2wal 1224 1
Colors of variables: wff set class
This axiom is referenced by:  gen2  1315  mpg  1316  mpgbi  1317  mpgbir  1318  hbth  1328  19.23h  1364  equidqeOLD  1403  19.9ht  1510  stdpc6  1569  equveli  1620  cesare  1982  camestres  1983  calemes  1994  ceqsralv  2558  vtocl2  2582  euxfr2dc  2699  sbcth  2750  sbciegf  2767  csbiegf  2863  sbcnestg  2872  csbnestg  2873  csbnest1g  2874  int0  3599  mpteq2ia  3813  mpteq2da  3816  ssopab2i  3984  relssi  4354  xpidtr  4638  funcnvsn  4867  tfrlem7  5851  tfrlemi14  5865  sucinc  5936  ch2var  7206  strcollnf  7399
  Copyright terms: Public domain W3C validator