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

Axiom ax-gen 1354
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 1445 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 1257 1 wff 𝑥𝜑
Colors of variables: wff set class
This axiom is referenced by:  gen2  1355  mpg  1356  mpgbi  1357  mpgbir  1358  hbth  1368  19.23h  1403  19.9ht  1548  stdpc6  1607  equveli  1658  cesare  2020  camestres  2021  calemes  2032  ceqsralv  2602  vtocl2  2626  euxfr2dc  2749  sbcth  2800  sbciegf  2817  csbiegf  2918  sbcnestg  2927  csbnestg  2928  csbnest1g  2929  int0  3657  mpteq2ia  3871  mpteq2da  3874  ssopab2i  4042  relssi  4459  xpidtr  4743  funcnvsn  4973  tfrlem7  5964  tfri1  5982  sucinc  6056  findcard  6376  findcard2  6377  findcard2s  6378  frec2uzzd  9350  frec2uzsucd  9351  frec2uzrand  9355  frec2uzf1od  9356  frecfzennn  9367  fclim  10046  ch2var  10294  strcollnf  10497
  Copyright terms: Public domain W3C validator