Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-11 GIF version

Axiom ax-11 1389
 Description: Axiom of Variable Substitution. One of the 5 equality axioms of predicate calculus. The final consequent ∀x(x = y → φ) is a way of expressing "y substituted for x in wff φ " (cf. sb6 1705). 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 1654 ("o" for "old") and was replaced with this shorter ax-11 1389 in Jan. 2007. The old axiom is proved from this one as theorem ax11o 1653. Conversely, this axiom is proved from ax-11o 1654 as theorem ax11 1655. Juha Arpiainen proved the independence of this axiom (in the form of the older axiom ax-11o 1654) 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 1654 (from which the ax-11 1389 instance follows by theorem ax11 1655.) The proof is by induction on formula length, using ax11eq 1810 and ax11el 1811 for the basis steps and ax11indn 1813, ax11indi 1814, and ax11inda 1818 for the induction steps. See also ax11v 1703 and ax11v2 1651 for other equivalents of this axiom that (unlike this axiom) have distinct variable restrictions.
Assertion
Ref Expression
ax-11 (x = y → (yφx(x = yφ)))

Detailed syntax breakdown of Axiom ax-11
StepHypRef Expression
1 vx . . 3 set x
2 vy . . 3 set y
31, 2weq 1384 . 2 wff x = y
4 wph . . . 4 wff φ
54, 2wal 1335 . . 3 wff yφ
63, 4wi 4 . . . 4 wff (x = yφ)
76, 1wal 1335 . . 3 wff x(x = yφ)
85, 7wi 4 . 2 wff (yφx(x = yφ))
93, 8wi 4 1 wff (x = y → (yφx(x = yφ)))
 Colors of variables: wff set class This axiom is referenced by:  a9wa9lem3  1407  a9wa9lem8  1413  a9wa9lem8OLD  1414  ax4  1423  ax10o  1575  equs5a  1631  ax11o  1653
 Copyright terms: Public domain W3C validator