Axiom ax-11 1764

Description: Axiom of Substitution. One of the 5 equality axioms of predicate calculus. The final consequent is a way of expressing " substituted for in wff " (cf. sb6 2182). It is based on Lemma 16 of [Tarski] p. 70 and Axiom C8 of [Monk2] p. 105, from which it can be proved by cases.

The original version of this axiom was ax-11o 2225 ("o" for "old") and was replaced with this shorter ax-11 1764 in Jan. 2007. The old axiom is proved from this one as theorem ax11o 2085. Conversely, this axiom is proved from ax-11o 2225 as theorem ax11 2239.

Juha Arpiainen proved the metalogical independence of this axiom (in the form of the older axiom ax-11o 2225) from the others on 19-Jan-2006. See item 9a at http://us.metamath.org/award2003.html.

See ax11v 2179 and ax11v2 2082 for other equivalents of this axiom that (unlike this axiom) have distinct variable restrictions.

This axiom scheme is logically redundant (see ax11w 1739) but is used as an auxiliary axiom to achieve metalogical completeness. (Contributed by NM, 22-Jan-2007.)

Assertion

Ref	Expression
ax-11

Detailed syntax breakdown of Axiom ax-11

Step	Hyp	Ref	Expression
1		vx	. . 3
2		vy	. . 3
3	1, 2	weq 1655	. 2
4		wph	. . . 4
5	4, 2	wal 1550	. . 3
6	3, 4	wi 4	. . . 4
7	6, 1	wal 1550	. . 3
8	5, 7	wi 4	. 2
9	3, 8	wi 4	1

This axiom is referenced by:  19.8a  1765  spOLD  1767  equs5a  1913  equs5e  1914  equs5eOLD  1915  ax10o2  2028  dvelimvOLD  2032  ax10oOLD  2043  a16gOLD  2053  ax11o  2085  ax11vALT  2180  dvelimvNEW7  29703  ax10oNEW7  29717  ax11oNEW7  29773  a16gNEW7  29787