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  5983  csbriotag  5985  abrexex2g  6282  opabex3d  6283  opabex3  6284  abrexex2  6286  dfoprab4f  6356  modom  6994  finexdc  7092  ssfirab  7129  uzind4s  9824  zsupcllemstep  10490  bezoutlemmain  12587  nnwosdc  12628  cbvrald  16435  bj-bdfindes  16595  bj-findes  16627