Theorem sbequ12 1698

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 1695	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑))
2		sbequ2 1696	. 2 ⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → 𝜑))
3	1, 2	impbid 127	1 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))

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

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 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443

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

This theorem is referenced by:  sbequ12r  1699  sbequ12a  1700  sbid  1701  ax16  1738  sb8h  1779  sb8eh  1780  sb8  1781  sb8e  1782  ax16ALT  1784  sbco  1887  sbcomxyyz  1891  sb9v  1899  sb6a  1909  mopick  2023  clelab  2209  sbab  2211  cbvralf  2580  cbvrexf  2581  cbvralsv  2597  cbvrexsv  2598  cbvrab  2613  sbhypf  2662  mob2  2786  reu2  2794  reu6  2795  sbcralt  2904  sbcrext  2905  sbcralg  2906  sbcreug  2908  cbvreucsf  2981  cbvrabcsf  2982  cbvopab1  3886  cbvopab1s  3888  csbopabg  3891  cbvmptf  3907  cbvmpt  3908  opelopabsb  4061  frind  4153  tfis  4371  findes  4391  opeliunxp  4461  ralxpf  4550  rexxpf  4551  cbviota  4951  csbiotag  4974  cbvriota  5579  csbriotag  5581  abrexex2g  5848  opabex3d  5849  opabex3  5850  abrexex2  5852  dfoprab4f  5920  finexdc  6570  ssfirab  6593  uzind4s  9010  zsupcllemstep  10823  bezoutlemmain  10869  cbvrald  11133  bj-bdfindes  11289  bj-findes  11321