Theorem sbequ12 1694

Description: An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
sbequ12	⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))

Proof of Theorem sbequ12

Step	Hyp	Ref	Expression
1		sbequ1 1691	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑))
2		sbequ2 1692	. 2 ⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → 𝜑))
3	1, 2	impbid 127	1 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 103  [wsb 1685

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 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440

This theorem depends on definitions:  df-bi 115  df-sb 1686

This theorem is referenced by:  sbequ12r  1695  sbequ12a  1696  sbid  1697  ax16  1734  sb8h  1775  sb8eh  1776  sb8  1777  sb8e  1778  ax16ALT  1780  sbco  1883  sbcomxyyz  1887  sb9v  1895  sb6a  1905  mopick  2019  clelab  2203  sbab  2205  cbvralf  2571  cbvrexf  2572  cbvralsv  2588  cbvrexsv  2589  cbvrab  2599  sbhypf  2648  mob2  2772  reu2  2780  reu6  2781  sbcralt  2890  sbcrext  2891  sbcralg  2892  sbcreug  2894  cbvreucsf  2966  cbvrabcsf  2967  cbvopab1  3851  cbvopab1s  3853  csbopabg  3856  cbvmpt  3872  opelopabsb  4015  frind  4107  tfis  4324  findes  4344  opeliunxp  4413  ralxpf  4500  rexxpf  4501  cbviota  4892  csbiotag  4915  cbvriota  5498  csbriotag  5500  abrexex2g  5767  opabex3d  5768  opabex3  5769  abrexex2  5771  dfoprab4f  5839  uzind4s  8678  zsupcllemstep  10341  bezoutlemmain  10387  cbvrald  10598  bj-bdfindes  10744  bj-findes  10776