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

Theorem sbequ12 2020
Description: An equality theorem for substitution. (Contributed by NM, 14-May-1993.)
Assertion
Ref Expression
sbequ12  |-  ( x  =  y  ->  ( ph 
<->  [ y  /  x ] ph ) )

Proof of Theorem sbequ12
StepHypRef Expression
1 sbequ1 2019 . 2  |-  ( x  =  y  ->  ( ph  ->  [ y  /  x ] ph ) )
2 sbequ2 1765 . 2  |-  ( x  =  y  ->  ( [ y  /  x ] ph  ->  ph ) )
31, 2impbid 191 1  |-  ( x  =  y  ->  ( ph 
<->  [ y  /  x ] ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   [wsb 1763
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-12 1878
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1634  df-sb 1764
This theorem is referenced by:  sbequ12r  2021  sbequ12a  2022  axc16ALT  2129  nfsb4t  2154  sbco2  2182  sb8  2191  sb8e  2192  sbal1  2228  2eu6OLD  2335  clelab  2546  clelabOLD  2547  sbab  2549  cbvralf  3027  cbvralsv  3044  cbvrexsv  3045  cbvrab  3056  sbhypf  3105  mob2  3228  reu2  3236  reu6  3237  sbcralt  3349  sbcreu  3353  cbvreucsf  3406  cbvrabcsf  3407  csbif  3934  rabasiun  4274  cbvopab1  4464  cbvopab1s  4466  cbvmptf  4484  cbvmpt  4485  opelopabsb  4699  csbopab  4721  csbopabgALT  4722  opeliunxp  4874  ralxpf  4969  cbviota  5537  csbiota  5561  cbvriota  6249  csbriota  6251  onminex  6624  tfis  6671  findes  6713  abrexex2g  6760  opabex3d  6761  opabex3  6762  abrexex2  6764  dfoprab4f  6841  uzind4s  11186  ac6sf2  27895  esumcvg  28519  bj-sbab  30921  wl-sb8t  31352  wl-sbalnae  31364  wl-ax11-lem8  31384  sbcrexgOLD  35060  pm13.193  36146  opeliun2xp  38414
  Copyright terms: Public domain W3C validator