Axiom ax-4 673

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 y is free in A.xx = y.) This is one of the 4 axioms of what we call "pure" predicate calculus. Unlike the more typical textbook Axiom of Specialization, we cannot choose a variable different from x for the special case. That is dealt with later when substitution is introduced - see stdpc4 869. 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 677. Conditional forms of the converse are given by ax-12 802, ax-15 806, ax-16 922, and ax-17 925.

Assertion

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

Detailed syntax breakdown of Axiom ax-4

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

This axiom is referenced by:  a4i 680  a4s 682  a4sd 683  19.20 690  19.8a 712  19.3r 714  19.12 729  19.21 738  19.21bi 742  19.38 760  19.21g 792  eq5 824  eqs1 828  sb2 859  sbied 903  hbsb4 905  hbsb4t 906  a16gb 934  sbal1 996  mopick 1054  2eu1 1067  2eu4 1070  ra4 1243  ralcom2 1314  ceqex 1410  axrep 1473  zfrep2 1475  ssopab2 2119  fununi 2705  fiint 3445  nd3 3734  axrepndlem2 3739  axrepnd 3740  axpowndlem2 3744  axpowndlem4 3746  axinfndlem1 3751  axacndlem4 3756  axacndlem5 3757  suppsrlem 4015

metamath.org