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

Axiom ax-11 1718
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 2040). 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 2085 ("o" for "old") and was replaced with this shorter ax-11 1718 in Jan. 2007. The old axiom is proved from this one as theorem ax11o 1939. Conversely, this axiom is proved from ax-11o 2085 as theorem ax11 2098.

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

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

This axiom scheme is logically redundant (see ax11w 1698) 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 1626 . 2  wff  x  =  y
4 wph . . . 4  wff  ph
54, 2wal 1529 . . 3  wff  A. y ph
63, 4wi 6 . . . 4  wff  ( x  =  y  ->  ph )
76, 1wal 1529 . . 3  wff  A. x
( x  =  y  ->  ph )
85, 7wi 6 . 2  wff  ( A. y ph  ->  A. x
( x  =  y  ->  ph ) )
93, 8wi 6 1  wff  ( x  =  y  ->  ( A. y ph  ->  A. x
( x  =  y  ->  ph ) ) )
Colors of variables: wff set class
This axiom is referenced by:  sp  1719  equs5a  1832  equs5e  1833  dvelimv  1883  ax10lem6  1887  a16gALT  1889  ax10o  1896  ax11o  1939  a12study4  28386  ax10lem17ALT  28392  a12study10  28405  a12study10n  28406  ax9lem3  28411  ax9lem17  28425
  Copyright terms: Public domain W3C validator