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