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

Theorem sbequ12 1670
Description: An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
sbequ12 (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))

Proof of Theorem sbequ12
StepHypRef Expression
1 sbequ1 1667 . 2 (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑))
2 sbequ2 1668 . 2 (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑𝜑))
31, 2impbid 124 1 (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102  [wsb 1661
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416
This theorem depends on definitions:  df-bi 114  df-sb 1662
This theorem is referenced by:  sbequ12r  1671  sbequ12a  1672  sbid  1673  ax16  1710  sb8h  1750  sb8eh  1751  sb8  1752  sb8e  1753  ax16ALT  1755  sbco  1858  sbcomxyyz  1862  sb9v  1870  sb6a  1880  mopick  1994  clelab  2178  sbab  2180  cbvralf  2544  cbvrexf  2545  cbvralsv  2561  cbvrexsv  2562  cbvrab  2572  sbhypf  2620  mob2  2744  reu2  2752  reu6  2753  sbcralt  2862  sbcrext  2863  sbcralg  2864  sbcreug  2866  cbvreucsf  2938  cbvrabcsf  2939  cbvopab1  3858  cbvopab1s  3860  csbopabg  3863  cbvmpt  3879  opelopabsb  4025  frind  4117  tfis  4334  findes  4354  opeliunxp  4423  ralxpf  4510  rexxpf  4511  cbviota  4900  csbiotag  4923  cbvriota  5506  csbriotag  5508  abrexex2g  5775  opabex3d  5776  opabex3  5777  abrexex2  5779  dfoprab4f  5847  uzind4s  8629  cbvrald  10314  bj-bdfindes  10461  bj-findes  10493
  Copyright terms: Public domain W3C validator