ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sbequ12 Unicode version

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

Proof of Theorem sbequ12
StepHypRef Expression
1 sbequ1 1692 . 2  |-  ( x  =  y  ->  ( ph  ->  [ y  /  x ] ph ) )
2 sbequ2 1693 . 2  |-  ( x  =  y  ->  ( [ y  /  x ] ph  ->  ph ) )
31, 2impbid 127 1  |-  ( x  =  y  ->  ( ph 
<->  [ y  /  x ] ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103   [wsb 1686
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441
This theorem depends on definitions:  df-bi 115  df-sb 1687
This theorem is referenced by:  sbequ12r  1696  sbequ12a  1697  sbid  1698  ax16  1735  sb8h  1776  sb8eh  1777  sb8  1778  sb8e  1779  ax16ALT  1781  sbco  1884  sbcomxyyz  1888  sb9v  1896  sb6a  1906  mopick  2020  clelab  2204  sbab  2206  cbvralf  2572  cbvrexf  2573  cbvralsv  2589  cbvrexsv  2590  cbvrab  2600  sbhypf  2649  mob2  2773  reu2  2781  reu6  2782  sbcralt  2891  sbcrext  2892  sbcralg  2893  sbcreug  2895  cbvreucsf  2967  cbvrabcsf  2968  cbvopab1  3859  cbvopab1s  3861  csbopabg  3864  cbvmpt  3880  opelopabsb  4023  frind  4115  tfis  4332  findes  4352  opeliunxp  4421  ralxpf  4510  rexxpf  4511  cbviota  4902  csbiotag  4925  cbvriota  5509  csbriotag  5511  abrexex2g  5778  opabex3d  5779  opabex3  5780  abrexex2  5782  dfoprab4f  5850  uzind4s  8759  zsupcllemstep  10485  bezoutlemmain  10531  cbvrald  10749  bj-bdfindes  10902  bj-findes  10934
  Copyright terms: Public domain W3C validator