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

Axiom ax-gen 1269
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 1361 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.)
Ref Expression
ax-g.1 φ
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 1266 1 wff xφ
Colors of variables: wff set class
This axiom is referenced by:  gen2  1270  mpg  1271  mpgbi  1272  mpgbir  1273  hbth  1283  19.23  1319  equidqeOLD  1357  19.9ht  1443  stdpc6  1481  cbv3h  1518  equveli  1526
  Copyright terms: Public domain W3C validator