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

Axiom ax-gen 1410
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 1501 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 1314 1 wff 𝑥𝜑
Colors of variables: wff set class
This axiom is referenced by:  gen2  1411  mpg  1412  mpgbi  1413  mpgbir  1414  hbth  1424  19.23h  1459  19.9ht  1605  stdpc6  1664  equveli  1717  cesare  2081  camestres  2082  calemes  2093  ceqsralv  2691  vtocl2  2715  euxfr2dc  2842  sbcth  2895  sbciegf  2912  csbiegf  3013  sbcnestg  3023  csbnestg  3024  csbnest1g  3025  int0  3755  mpteq2ia  3984  mpteq2da  3987  ssopab2i  4169  relssi  4600  xpidtr  4899  funcnvsn  5138  funinsn  5142  tfrlem7  6182  tfri1  6230  sucinc  6309  findcard  6750  findcard2  6751  findcard2s  6752  fiintim  6785  fisseneq  6788  frec2uzrand  10133  frec2uzf1od  10134  frecfzennn  10154  hashinfom  10479  zfz1iso  10539  fclim  11018  distop  12165  ch2var  12870  strcollnf  13079
  Copyright terms: Public domain W3C validator