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 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559

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  2358  sbab  2360  nfabdw  2394  cbvralf  2759  cbvrexf  2760  cbvralsv  2784  cbvrexsv  2785  cbvrab  2801  sbhypf  2854  mob2  2987  reu2  2995  reu6  2996  sbcralt  3109  sbcrext  3110  sbcralg  3111  sbcreug  3113  cbvreucsf  3193  cbvrabcsf  3194  cbvopab1  4167  cbvopab1s  4169  csbopabg  4172  cbvmptf  4188  cbvmpt  4189  opelopabsb  4360  frind  4455  tfis  4687  findes  4707  opeliunxp  4787  ralxpf  4882  rexxpf  4883  cbviota  5298  csbiotag  5326  cbvriota  5993  csbriotag  5995  abrexex2g  6291  opabex3d  6292  opabex3  6293  abrexex2  6295  dfoprab4f  6365  modom  7037  finexdc  7135  ssfirab  7172  uzind4s  9885  zsupcllemstep  10552  bezoutlemmain  12649  nnwosdc  12690  cbvrald  16506  bj-bdfindes  16665  bj-findes  16697