Axiom ax-gen 677

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 680 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

Step	Hyp	Ref	Expression
1		wph	. 2 wff φ
2		vx	. 2 set x
3	1, 2	wal 672	1 wff ∀xφ

This axiom is referenced by:  gen2 681  mpg 684  hbth 697  cbv3 847  cbval 848  rgen2 1248  vtocl2 1379  mosub 1433  int0 1978  ssopab2i 2120  supmo 2156  ordom 2382  relssi 2481  cleqreli 2484  dmcosseq 2572  funsn 2690  fconst 2774  fvex 2838  tfrlem7 2955  tfrlem8 2956  caoprmo 3084  pssnn 3428  fiint 3445  inf0 3457  inf4 3473  trcl 3489  axpowndlem2 3744  axpowndlem4 3746  axregndlem2 3749  axinfnd 3752  suppsr3 4018  nnssre 4425  nnind 4434

metamath.org