Theorem sbequ12 2252

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

Syntax hints:   → wi 4   ↔ wb 206  [wsb 2065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066

This theorem is referenced by:  sbequ12r  2253  sbequ12a  2255  sb8ef  2353  sbbib  2359  axc16ALT  2487  nfsb4t  2497  sbco2  2509  sb8  2515  sb8e  2516  sbal1  2526  sbal2  2527  sbab  2875  cbvrexsvw  3291  cbvralsvwOLD  3292  cbvralsvwOLDOLD  3293  cbvrexsvwOLD  3294  cbvralf  3334  cbvralsv  3340  cbvrexsv  3341  cbvrabwOLD  3442  cbvrab  3446  sbhypfOLD  3511  mob2  3686  reu2  3696  reu6  3697  sbcralt  3835  sbcreu  3839  cbvrabcsfw  3903  cbvreucsf  3906  cbvrabcsf  3907  csbif  4546  cbvopab1  5181  cbvopab1g  5182  cbvopab1s  5184  cbvmptf  5207  cbvmptfg  5208  csbopab  5515  csbopabgALT  5516  opeliunxp  5705  opeliun2xp  5706  ralxpf  5810  cbviotaw  6471  cbviota  6473  csbiota  6504  f1ossf1o  7100  cbvriotaw  7353  cbvriota  7357  csbriota  7359  onminex  7778  tfis  7831  findes  7876  abrexex2g  7943  opabex3d  7944  opabex3rd  7945  opabex3  7946  dfoprab4f  8035  uzind4s  12867  ac6sf2  32548  esumcvg  34076  wl-sb8t  37540  wl-sbalnae  37550  wl-ax11-lem8  37580  sbcrexgOLD  42773  scottabes  44231  pm13.193  44400  2reu8i  47114  ichnfimlem  47464