Theorem sbequ12 1819

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

Syntax hints:   → wi 4   ↔ wb 105  [wsb 1810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558

This theorem depends on definitions:  df-bi 117  df-sb 1811

This theorem is referenced by:  sbequ12r  1820  sbequ12a  1821  sbid  1822  ax16  1861  sb8h  1902  sb8eh  1903  sb8  1904  sb8e  1905  ax16ALT  1907  sbco  2021  sbcomxyyz  2025  sb9v  2031  sb6a  2041  mopick  2158  clelab  2357  sbab  2359  nfabdw  2393  cbvralf  2758  cbvrexf  2759  cbvralsv  2783  cbvrexsv  2784  cbvrab  2800  sbhypf  2853  mob2  2986  reu2  2994  reu6  2995  sbcralt  3108  sbcrext  3109  sbcralg  3110  sbcreug  3112  cbvreucsf  3192  cbvrabcsf  3193  cbvopab1  4162  cbvopab1s  4164  csbopabg  4167  cbvmptf  4183  cbvmpt  4184  opelopabsb  4354  frind  4449  tfis  4681  findes  4701  opeliunxp  4781  ralxpf  4876  rexxpf  4877  cbviota  5291  csbiotag  5319  cbvriota  5982  csbriotag  5984  abrexex2g  6281  opabex3d  6282  opabex3  6283  abrexex2  6285  dfoprab4f  6355  modom  6993  finexdc  7091  ssfirab  7128  uzind4s  9823  zsupcllemstep  10488  bezoutlemmain  12568  nnwosdc  12609  cbvrald  16384  bj-bdfindes  16544  bj-findes  16576