Theorem sbequ12 2245

Description: An equality theorem for substitution. (Contributed by NM, 14-May-1993.)

Assertion

Ref	Expression
sbequ12	⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))

Proof of Theorem sbequ12

Step	Hyp	Ref	Expression
1		sbequ1 2241	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑))
2		sbequ2 2242	. 2 ⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → 𝜑))
3	1, 2	impbid 211	1 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 205  [wsb 2068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2069

This theorem is referenced by:  sbequ12r  2246  sbequ12a  2248  sb5OLD  2270  sb8fOLD  2353  sb8ef  2354  sbbib  2360  axc16ALT  2494  nfsb4t  2504  sbco2  2516  sb8  2522  sb8e  2523  sbal1  2534  sbal2  2535  clelabOLD  2885  sbab  2887  nfabdwOLD  2932  cbvralfwOLD  3370  cbvralf  3372  cbvralsvw  3403  cbvrexsvw  3404  cbvralsv  3405  cbvrexsv  3406  cbvrabw  3425  cbvrab  3426  sbhypf  3492  mob2  3651  reu2  3661  reu6  3662  sbcralt  3806  sbcreu  3810  cbvrabcsfw  3877  cbvreucsf  3880  cbvrabcsf  3881  csbif  4517  cbvopab1  5150  cbvopab1g  5151  cbvopab1s  5153  cbvmptf  5184  cbvmptfg  5185  csbopab  5469  csbopabgALT  5470  opeliunxp  5655  ralxpf  5758  cbviotaw  6402  cbviota  6405  csbiota  6430  f1ossf1o  7009  cbvriotaw  7250  cbvriota  7255  csbriota  7257  onminex  7661  tfis  7710  findes  7758  abrexex2g  7816  opabex3d  7817  opabex3rd  7818  opabex3  7819  dfoprab4f  7905  uzind4s  12657  ac6sf2  30969  esumcvg  32063  wl-sb8t  35716  wl-sbalnae  35726  wl-ax11-lem8  35752  sbcrexgOLD  40614  scottabes  41867  pm13.193  42036  2reu8i  44616  ichnfimlem  44926  opeliun2xp  45679