Theorem sbequ12 2250

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

Syntax hints:   → wi 4   ↔ wb 209  [wsb 2069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070

This theorem is referenced by:  sbequ12r  2251  sbequ12a  2253  sb5  2273  sb8v  2362  sb8ev  2363  sbbib  2369  axc16ALT  2507  nfsb4t  2517  sbco2  2530  sb8  2536  sb8e  2537  sbal1  2548  sbal2  2549  clelab  2933  sbab  2935  nfabdw  2976  cbvralfwOLD  3383  cbvralf  3385  cbvralsvw  3414  cbvrexsvw  3415  cbvralsv  3416  cbvrexsv  3417  cbvrabw  3437  cbvrab  3438  sbhypf  3500  mob2  3654  reu2  3664  reu6  3665  sbcralt  3801  sbcreu  3805  cbvrabcsfw  3869  cbvreucsf  3872  cbvrabcsf  3873  csbif  4480  cbvopab1  5103  cbvopab1g  5104  cbvopab1s  5106  cbvmptf  5129  cbvmptfg  5130  opelopabsb  5382  csbopab  5407  csbopabgALT  5408  opeliunxp  5583  ralxpf  5681  cbviotaw  6290  cbviota  6292  csbiota  6317  f1ossf1o  6867  cbvriotaw  7102  cbvriota  7106  csbriota  7108  onminex  7502  tfis  7549  findes  7593  abrexex2g  7647  opabex3d  7648  opabex3rd  7649  opabex3  7650  dfoprab4f  7736  uzind4s  12296  ac6sf2  30384  esumcvg  31455  wl-sb8t  34953  wl-sbalnae  34963  wl-ax11-lem8  34989  sbcrexgOLD  39726  scottabes  40950  pm13.193  41115  2reu8i  43669  ichnfimlem  43980  opeliun2xp  44734