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

Axiom ax-gen 1253
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 1342 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 1250 1 wff xφ
Colors of variables: wff set class
This axiom is referenced by:  gen2  1254  mpg  1255  mpgbi  1256  mpgbir  1257  hbth  1267  19.23  1303  equidqeOLD  1338  19.9ht  1420  stdpc6  1458  cbv3  1495  equveli  1501  ax5o  1889  ax5  1891  ax4  1892  ax11eq  1897  a12lem1  1909
  Copyright terms: Public domain W3C validator