Theorem sbequ12 1817

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

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

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 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556

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

This theorem is referenced by:  sbequ12r  1818  sbequ12a  1819  sbid  1820  ax16  1859  sb8h  1900  sb8eh  1901  sb8  1902  sb8e  1903  ax16ALT  1905  sbco  2019  sbcomxyyz  2023  sb9v  2029  sb6a  2039  mopick  2156  clelab  2355  sbab  2357  nfabdw  2391  cbvralf  2756  cbvrexf  2757  cbvralsv  2781  cbvrexsv  2782  cbvrab  2797  sbhypf  2850  mob2  2983  reu2  2991  reu6  2992  sbcralt  3105  sbcrext  3106  sbcralg  3107  sbcreug  3109  cbvreucsf  3189  cbvrabcsf  3190  cbvopab1  4157  cbvopab1s  4159  csbopabg  4162  cbvmptf  4178  cbvmpt  4179  opelopabsb  4348  frind  4443  tfis  4675  findes  4695  opeliunxp  4774  ralxpf  4868  rexxpf  4869  cbviota  5283  csbiotag  5311  cbvriota  5972  csbriotag  5974  abrexex2g  6271  opabex3d  6272  opabex3  6273  abrexex2  6275  dfoprab4f  6345  finexdc  7073  ssfirab  7109  uzind4s  9797  zsupcllemstep  10461  bezoutlemmain  12534  nnwosdc  12575  cbvrald  16207  bj-bdfindes  16367  bj-findes  16399