Metamath Proof Explorer


Axiom ax-gen

Description: Rule of (universal) generalization. In our axiomatization, this is the only postulated (that is, axiomatic) rule of inference of predicate calculus (together with the rule of modus ponens ax-mp of propositional 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 , then we can conclude A. x x = x or even A. y x = x . Theorem altru shows the special case A. x T. . The converse rule of inference spi (universal instantiation, or universal specialization) shows that we can also go the other way: in other words, we can add or remove universal quantifiers from the beginning of any theorem as required. Note that the closed form ( ph -> A. x ph ) need not hold (but may hold in special cases, see ax-5 ). (Contributed by NM, 3-Jan-1993)

Ref Expression
Hypothesis ax-gen.1 𝜑
Assertion ax-gen 𝑥 𝜑

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx 𝑥
1 wph 𝜑
2 1 0 wal 𝑥 𝜑