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

Axiom ax-gen 1311
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 1402 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 1221 1
Colors of variables: wff set class
This axiom is referenced by:  gen2  1312  mpg  1313  mpgbi  1314  mpgbir  1315  hbth  1325  19.23h  1360  19.9ht  1505  stdpc6  1564  equveli  1615  cesare  1977  camestres  1978  calemes  1989  ceqsralv  2553  vtocl2  2577  euxfr2dc  2694  sbcth  2745  sbciegf  2762  csbiegf  2858  sbcnestg  2867  csbnestg  2868  csbnest1g  2869  int0  3592  mpteq2ia  3806  mpteq2da  3809  ssopab2i  3977  relssi  4346  xpidtr  4630  funcnvsn  4859  tfrlem7  5843  tfrlemi14  5857  sucinc  5928  ch2var  8172  strcollnf  8365
  Copyright terms: Public domain W3C validator