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

Axiom ax-gen 1270
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 a4i 1363 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 1267 1 wff xφ
Colors of variables: wff set class
This axiom is referenced by:  gen2  1271  mpg  1272  mpgbi  1273  mpgbir  1274  hbth  1284  19.23  1320  equidqeOLD  1359  19.9ht  1458  stdpc6  1504  equveli  1552  ceqsralv  2388  vtocl2  2412
  Copyright terms: Public domain W3C validator