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 A.xx = x or even A.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	|- ph

Assertion

Ref	Expression
ax-gen	|- A.xph

Detailed syntax breakdown of Axiom ax-gen

Step	Hyp	Ref	Expression
1		wph	. 2 wff ph
2		vx	. 2 set x
3	1, 2	wal 1335	1 wff A.xph

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