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

Theorem sbequ12 1636
Description: An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
sbequ12 (x = y → (φ ↔ [y / x]φ))

Proof of Theorem sbequ12
StepHypRef Expression
1 sbequ1 1633 . 2 (x = y → (φ → [y / x]φ))
2 sbequ2 1634 . 2 (x = y → ([y / x]φφ))
31, 2impbid 120 1 (x = y → (φ ↔ [y / x]φ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98  [wsb 1627
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-4 1381
This theorem depends on definitions:  df-bi 110  df-sb 1628
This theorem is referenced by:  sbequ12r  1637  sbequ12a  1638  sbid  1639  ax16  1676  sb8h  1716  sb8eh  1717  sb8  1718  sb8e  1719  ax16ALT  1721  sbco  1824  sbcomxyyz  1828  sb9v  1836  sb6a  1846  mopick  1960  clelab  2144  sbab  2146  cbvralf  2505  cbvrexf  2506  cbvralsv  2522  cbvrexsv  2523  cbvrab  2533  sbhypf  2580  mob2  2698  reu2  2706  reu6  2707  sbcralt  2811  sbcrext  2812  sbcralg  2813  sbcrexg  2814  sbcreug  2815  cbvreucsf  2887  cbvrabcsf  2888  cbvopab1  3804  cbvopab1s  3806  csbopabg  3809  cbvmpt  3825  opelopabsb  3971  tfis  4233  findes  4253  opeliunxp  4322  ralxpf  4409  rexxpf  4410  cbviota  4799  csbiotag  4822  cbvriota  5402  csbriotag  5404  abrexex2g  5670  opabex3d  5671  opabex3  5672  abrexex2  5674  dfoprab4f  5742  cbvrald  7034  bj-bdfindes  7171  bj-findes  7199
  Copyright terms: Public domain W3C validator