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

Axiom ax-gen 1269
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 1360 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 1266 1 wff xφ
Colors of variables: wff set class
This axiom is referenced by:  gen2  1270  mpg  1271  mpgbi  1272  mpgbir  1273  hbth  1283  19.23  1319  equidqeOLD  1356  19.9ht  1438  stdpc6  1476  cbv3  1512  equveli  1518  ax5o  1912  ax5  1914  ax4  1915  ax11eq  1920  a12lem1  1932
  Copyright terms: Public domain W3C validator