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 A.xx = x or even A.yx = x. Theorem a4i 1361 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	|- 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 1266	1 wff A.xph

This axiom is referenced by:  gen2  1270  mpg  1271  mpgbi  1272  mpgbir  1273  hbth  1283  19.23  1319  equidqeOLD  1357  19.9ht  1443  stdpc6  1481  cbv3h  1518  equveli  1526