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

Axiom ax-gen 1257
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 1335 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 1253 1 wff xφ
Colors of variables: wff set class
This axiom is referenced by:  gen2  1258  mpg  1259  mpgbi  1260  mpgbir  1261  hbth  1273  19.23  1297  equidqeOLD  1324  ax4  1326  ax5o  1327  ax5  1329  ax6  1332  19.9t  1410  stdpc6  1442  cbv3  1476  equveli  1482  ax11eq  1786  a12lem1  1798
  Copyright terms: Public domain W3C validator