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

Axiom ax-11 1757
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 2152). 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 2195 ("o" for "old") and was replaced with this shorter ax-11 1757 in Jan. 2007. The old axiom is proved from this one as theorem ax11o 2051. Conversely, this axiom is proved from ax-11o 2195 as theorem ax11 2209.

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

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

This axiom scheme is logically redundant (see ax11w 1732) 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  1758  spOLD  1760  equs5a  1905  equs5e  1906  equs5eOLD  1907  ax10lem3  1990  dvelimvOLD  1994  ax10oOLD  2005  a16gOLD  2015  ax11o  2051  ax11vALT  2150  axi11e  2386  dvelimvNEW7  29172  ax10oNEW7  29186  ax11oNEW7  29240  a16gNEW7  29254
  Copyright terms: Public domain W3C validator