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

Axiom ax-gen 1379
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 1470 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 1283 1 wff 𝑥𝜑
Colors of variables: wff set class
This axiom is referenced by:  gen2  1380  mpg  1381  mpgbi  1382  mpgbir  1383  hbth  1393  19.23h  1428  19.9ht  1573  stdpc6  1632  equveli  1684  cesare  2047  camestres  2048  calemes  2059  ceqsralv  2641  vtocl2  2665  euxfr2dc  2788  sbcth  2839  sbciegf  2856  csbiegf  2957  sbcnestg  2966  csbnestg  2967  csbnest1g  2968  int0  3676  mpteq2ia  3890  mpteq2da  3893  ssopab2i  4067  relssi  4486  xpidtr  4776  funcnvsn  5011  funinsn  5015  tfrlem7  6013  tfri1  6061  sucinc  6137  findcard  6533  findcard2  6534  findcard2s  6535  fisseneq  6566  frec2uzrand  9700  frec2uzf1od  9701  frecfzennn  9721  hashinfom  10020  fclim  10506  ch2var  11010  strcollnf  11222
  Copyright terms: Public domain W3C validator