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  3288  cbvralsvwOLD  3289  cbvralsvwOLDOLD  3290  cbvrexsvwOLD  3291  cbvralf  3331  cbvralsv  3337  cbvrexsv  3338  cbvrabwOLD  3439  cbvrab  3443  sbhypfOLD  3508  mob2  3683  reu2  3693  reu6  3694  sbcralt  3832  sbcreu  3836  cbvrabcsfw  3900  cbvreucsf  3903  cbvrabcsf  3904  csbif  4542  cbvopab1  5176  cbvopab1g  5177  cbvopab1s  5179  cbvmptf  5202  cbvmptfg  5203  csbopab  5510  csbopabgALT  5511  opeliunxp  5698  opeliun2xp  5699  ralxpf  5800  cbviotaw  6459  cbviota  6461  csbiota  6492  f1ossf1o  7082  cbvriotaw  7335  cbvriota  7339  csbriota  7341  onminex  7758  tfis  7811  findes  7856  abrexex2g  7922  opabex3d  7923  opabex3rd  7924  opabex3  7925  dfoprab4f  8014  uzind4s  12843  ac6sf2  32521  esumcvg  34049  wl-sb8t  37513  wl-sbalnae  37523  wl-ax11-lem8  37553  sbcrexgOLD  42746  scottabes  44204  pm13.193  44373  2reu8i  47087  ichnfimlem  47437