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

Axiom ax-11 1753
Description: Axiom of Substitution. One of the 5 equality axioms of predicate calculus. The final consequent  A. x ( x  =  y  ->  ph ) is a way of expressing " y substituted for  x in wff  ph " (cf. sb6 2125). 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 2168 ("o" for "old") and was replaced with this shorter ax-11 1753 in Jan. 2007. The old axiom is proved from this one as theorem ax11o 2020. Conversely, this axiom is proved from ax-11o 2168 as theorem ax11 2182.

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

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

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

Assertion
Ref Expression
ax-11  |-  ( x  =  y  ->  ( A. y ph  ->  A. x
( x  =  y  ->  ph ) ) )

Detailed syntax breakdown of Axiom ax-11
StepHypRef Expression
1 vx . . 3  set  x
2 vy . . 3  set  y
31, 2weq 1650 . 2  wff  x  =  y
4 wph . . . 4  wff  ph
54, 2wal 1546 . . 3  wff  A. y ph
63, 4wi 4 . . . 4  wff  ( x  =  y  ->  ph )
76, 1wal 1546 . . 3  wff  A. x
( x  =  y  ->  ph )
85, 7wi 4 . 2  wff  ( A. y ph  ->  A. x
( x  =  y  ->  ph ) )
93, 8wi 4 1  wff  ( x  =  y  ->  ( A. y ph  ->  A. x
( x  =  y  ->  ph ) ) )
Colors of variables: wff set class
This axiom is referenced by:  19.8a  1754  spOLD  1756  equs5a  1898  equs5e  1899  equs5eOLD  1900  dvelimvOLD  1972  ax10lem6  1975  a16g  1977  ax10o  1983  ax11o  2020  ax11vALT  2123  axi11e  2359  dvelimvNEW7  28793  ax10oNEW7  28807  ax11oNEW7  28861  a16gNEW7  28875  a12study4  29093  ax10lem17ALT  29099  a12study10  29112  a12study10n  29113  ax9lem3  29118  ax9lem17  29132
  Copyright terms: Public domain W3C validator