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

Axiom ax-gen 1408
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 1499 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 1312 1  wff  A. x ph
Colors of variables: wff set class
This axiom is referenced by:  gen2  1409  mpg  1410  mpgbi  1411  mpgbir  1412  hbth  1422  19.23h  1457  19.9ht  1603  stdpc6  1662  equveli  1715  cesare  2079  camestres  2080  calemes  2091  ceqsralv  2689  vtocl2  2713  euxfr2dc  2840  sbcth  2893  sbciegf  2910  csbiegf  3011  sbcnestg  3021  csbnestg  3022  csbnest1g  3023  int0  3753  mpteq2ia  3982  mpteq2da  3985  ssopab2i  4167  relssi  4598  xpidtr  4897  funcnvsn  5136  funinsn  5140  tfrlem7  6180  tfri1  6228  sucinc  6307  findcard  6748  findcard2  6749  findcard2s  6750  fiintim  6783  fisseneq  6786  frec2uzrand  10118  frec2uzf1od  10119  frecfzennn  10139  hashinfom  10464  zfz1iso  10524  fclim  11003  distop  12149  ch2var  12785  strcollnf  12994
  Copyright terms: Public domain W3C validator