Axiom ax-4 1521

Description: Axiom of Specialization. A quantified wff implies the wff without a quantifier (i.e. an instance, or special case, of the generalized wff). In other words if something is true for all x, it is true for any specific x (that would typically occur as a free variable in the wff substituted for ph). (A free variable is one that does not occur in the scope of a quantifier: x and y are both free in x = y, but only x is free in A. y x = y.) Axiom scheme C5' in [Megill] p. 448 (p. 16 of the preprint). Also appears as Axiom B5 of [Tarski] p. 67 (under his system S2, defined in the last paragraph on p. 77).

Note that the converse of this axiom does not hold in general, but a weaker inference form of the converse holds and is expressed as rule ax-gen 1460. Conditional forms of the converse are given by ax12 1523, ax-16 1825, and ax-17 1537.

Unlike the more general textbook Axiom of Specialization, we cannot choose a variable different from x for the special case. For use, that requires the assistance of equality axioms, and we deal with it later after we introduce the definition of proper substitution - see stdpc4 1786.

(Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
ax-4	|- ( A. x ph -> ph )

Detailed syntax breakdown of Axiom ax-4

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 setvar x
3	1, 2	wal 1362	. 2 wff A. x ph
4	3, 1	wi 4	1 wff ( A. x ph -> ph )

This axiom is referenced by:  sp  1522  ax12  1523  hbequid  1524  spi  1547  hbim  1556  19.3h  1564  19.21h  1568  19.21bi  1569  hbimd  1584  19.21ht  1592  hbnt  1664  19.12  1676  19.38  1687  ax9o  1709  hbae  1729  equveli  1770  sb2  1778  drex1  1809  ax11b  1837  a16gb  1876  sb56  1897  sb6  1898  sbalyz  2015  hbsb4t  2029  moim  2106  mopick  2120