Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-11 Unicode version

Axiom ax-11 1624
 Description: Axiom of Variable Substitution. One of the 5 equality axioms of predicate calculus. The final consequent is a way of expressing " substituted for in wff " (cf. sb6 1993). 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 1941 ("o" for "old") and was replaced with this shorter ax-11 1624 in Jan. 2007. The old axiom is proved from this one as theorem ax11o 1940. Conversely, this axiom is proved from ax-11o 1941 as theorem ax11 1942. Juha Arpiainen proved the independence of this axiom (in the form of the older axiom ax-11o 1941) from the others on 19-Jan-2006. See item 9a at http://us.metamath.org/award2003.html. Interestingly, if the wff expression substituted for contains no wff variables, the resulting statement can be proved without invoking this axiom. This means that even though this axiom is metalogically independent from the others, it is not logically independent. Specifically, we can prove any wff-variable-free instance of axiom ax-11o 1941 (from which the ax-11 1624 instance follows by theorem ax11 1942.) The proof is by induction on formula length, using ax11eq 2108 and ax11el 2109 for the basis steps and ax11indn 2111, ax11indi 2112, and ax11inda 2116 for the induction steps. (This paragraph is true provided we use ax-10o 1836 in place of ax-10 1678.) See also ax11v 1991 and ax11v2 1936 for other equivalents of this axiom that (unlike this axiom) have distinct variable restrictions. (Contributed by NM, 22-Jan-2007.)
Assertion
Ref Expression
ax-11

Detailed syntax breakdown of Axiom ax-11
StepHypRef Expression
1 vx . . 3
2 vy . . 3
31, 2weq 1620 . 2
4 wph . . . 4
54, 2wal 1532 . . 3
63, 4wi 6 . . . 4
76, 1wal 1532 . . 3
85, 7wi 6 . 2
93, 8wi 6 1
 Colors of variables: wff set class This axiom is referenced by:  ax12o10lem3  1637  ax10lem23  1672  ax10lem24  1673  a16gALT  1679  ax4  1691  ax10o  1835  equs5a  1912  equs5e  1913  ax11o  1940  ax12o10lem3X  28185  ax10lem23X  28243  ax10lem24X  28244  a16gALTX  28249  a12study4  28268  ax10lem17ALT  28274  a12study10  28287  a12study10n  28288  ax9lem3  28293  ax9lem17  28307
 Copyright terms: Public domain W3C validator