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

Axiom ax-gen 1243
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 1331 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 1240 1 wff xφ
Colors of variables: wff set class
This axiom is referenced by:  gen2  1244  mpg  1245  mpgbi  1246  mpgbir  1247  hbth  1257  19.23  1293  equidqeOLD  1327  19.9ht  1408  stdpc6  1445  cbv3  1482  equveli  1488  ax5o  1874  ax5  1876  ax4  1877  ax11eq  1882  a12lem1  1894
  Copyright terms: Public domain W3C validator