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

Axiom ax-gen 1235
Description: Rule of Generalization. The postulated inference rule of pure 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 1312 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 1231 1 wff xφ
Colors of variables: wff set class
This axiom is referenced by:  gen2  1236  mpg  1237  mpgbi  1238  mpgbir  1239  hbth  1251  19.23  1275  equidqeOLD  1302  ax5o  1304  ax5  1306  ax6  1309  19.9t  1385  stdpc6  1414  cbv3  1450  equveli  1456  ax4  1809  ax11eq  1811  a12lem1  1823
  Copyright terms: Public domain W3C validator