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

Axiom ax-gen 1274
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 xx = x or even yx = x. Theorem spi 1367 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 xφ

Detailed syntax breakdown of Axiom ax-gen
StepHypRef Expression
1 wph . 2 wff φ
2 vx . 2 set x
31, 2wal 1271 1 wff xφ
Colors of variables: wff set class
This axiom is referenced by:  gen2  1275  mpg  1276  mpgbi  1277  mpgbir  1278  hbth  1288  19.23  1324  equidqeOLD  1363  19.9ht  1462  stdpc6  1509  equveli  1560  ceqsralv  2445  vtocl2  2469  euxfr2dc  2583
  Copyright terms: Public domain W3C validator