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

Theorem sbequ12 1727
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 1724 . 2  |-  ( x  =  y  ->  ( ph  ->  [ y  /  x ] ph ) )
2 sbequ2 1725 . 2  |-  ( x  =  y  ->  ( [ y  /  x ] ph  ->  ph ) )
31, 2impbid 128 1  |-  ( x  =  y  ->  ( ph 
<->  [ y  /  x ] ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104   [wsb 1718
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470
This theorem depends on definitions:  df-bi 116  df-sb 1719
This theorem is referenced by:  sbequ12r  1728  sbequ12a  1729  sbid  1730  ax16  1767  sb8h  1808  sb8eh  1809  sb8  1810  sb8e  1811  ax16ALT  1813  sbco  1917  sbcomxyyz  1921  sb9v  1929  sb6a  1939  mopick  2053  clelab  2240  sbab  2242  cbvralf  2623  cbvrexf  2624  cbvralsv  2640  cbvrexsv  2641  cbvrab  2656  sbhypf  2707  mob2  2835  reu2  2843  reu6  2844  sbcralt  2955  sbcrext  2956  sbcralg  2957  sbcreug  2959  cbvreucsf  3032  cbvrabcsf  3033  cbvopab1  3969  cbvopab1s  3971  csbopabg  3974  cbvmptf  3990  cbvmpt  3991  opelopabsb  4150  frind  4242  tfis  4465  findes  4485  opeliunxp  4562  ralxpf  4653  rexxpf  4654  cbviota  5061  csbiotag  5084  cbvriota  5706  csbriotag  5708  abrexex2g  5984  opabex3d  5985  opabex3  5986  abrexex2  5988  dfoprab4f  6057  finexdc  6762  ssfirab  6788  uzind4s  9337  zsupcllemstep  11545  bezoutlemmain  11593  cbvrald  12829  bj-bdfindes  12981  bj-findes  13013
  Copyright terms: Public domain W3C validator