MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbequ12r Structured version   Unicode version

Theorem sbequ12r 1948
Description: An equality theorem for substitution. (Contributed by NM, 6-Oct-2004.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
Assertion
Ref Expression
sbequ12r  |-  ( x  =  y  ->  ( [ x  /  y ] ph  <->  ph ) )

Proof of Theorem sbequ12r
StepHypRef Expression
1 sbequ12 1947 . . 3  |-  ( y  =  x  ->  ( ph 
<->  [ x  /  y ] ph ) )
21bicomd 201 . 2  |-  ( y  =  x  ->  ( [ x  /  y ] ph  <->  ph ) )
32equcoms 1735 1  |-  ( x  =  y  ->  ( [ x  /  y ] ph  <->  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   [wsb 1702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-sb 1703
This theorem is referenced by:  sbequ12a  1949  sbid  1951  sbidmOLD  2119  sb5rf  2129  sb6rf  2131  2sb5rf  2167  2sb6rf  2168  abbiOLD  2584  opeliunxp  4993  isarep1  5600  findes  6611  axrepndlem1  8862  axrepndlem2  8863  nn0min  26230  esumcvg  26675  wl-nfs1t  28510  wl-sb6rft  28516  wl-equsb4  28524  wl-ax11-lem5  28548  sbcalf  29063  sbcexf  29064  opeliun2xp  30863  bj-abbi  32609
  Copyright terms: Public domain W3C validator