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

Axiom ax-gen 1381
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  x  =  x, we can conclude  A. x x  =  x or even  A. y
x  =  x. Theorem spi 1472 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  |-  ph
Assertion
Ref Expression
ax-gen  |-  A. x ph

Detailed syntax breakdown of Axiom ax-gen
StepHypRef Expression
1 wph . 2  wff  ph
2 vx . 2  setvar  x
31, 2wal 1285 1  wff  A. x ph
Colors of variables: wff set class
This axiom is referenced by:  gen2  1382  mpg  1383  mpgbi  1384  mpgbir  1385  hbth  1395  19.23h  1430  19.9ht  1575  stdpc6  1634  equveli  1686  cesare  2049  camestres  2050  calemes  2061  ceqsralv  2644  vtocl2  2668  euxfr2dc  2791  sbcth  2842  sbciegf  2859  csbiegf  2960  sbcnestg  2970  csbnestg  2971  csbnest1g  2972  int0  3685  mpteq2ia  3899  mpteq2da  3902  ssopab2i  4078  relssi  4497  xpidtr  4789  funcnvsn  5024  funinsn  5028  tfrlem7  6036  tfri1  6084  sucinc  6160  findcard  6556  findcard2  6557  findcard2s  6558  fisseneq  6592  frec2uzrand  9740  frec2uzf1od  9741  frecfzennn  9761  hashinfom  10083  zfz1iso  10143  fclim  10577  ch2var  11113  strcollnf  11325
  Copyright terms: Public domain W3C validator