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

Axiom ax-gen 1339
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 1432 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.
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 1335 1 wff xφ
Colors of variables: wff set class
This axiom is referenced by:  gen2  1340  mpg  1341  mpgbi  1342  mpgbir  1343  hbth  1355  19.23  1379  hbequidOLD  1398  equidqeOLD  1420  ax4  1423  ax5o  1424  ax5  1426  ax6  1429  19.9t  1530  stdpc6  1563  cbv3  1597  equveli  1603  ax11eq  1810  a12lem1  1823
  Copyright terms: Public domain W3C validator