Theorem sbequ12 2258

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2184

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068

This theorem is referenced by:  sbequ12r  2259  sbequ12a  2261  sb8ef  2359  sbbib  2365  axc16ALT  2493  nfsb4t  2503  sbco2  2515  sb8  2521  sb8e  2522  sbal1  2532  sbal2  2533  sbab  2882  cbvrexsvw  3288  cbvralsvwOLD  3289  cbvralsvwOLDOLD  3290  cbvrexsvwOLD  3291  cbvralf  3330  cbvralsv  3336  cbvrexsv  3337  cbvrabwOLD  3435  cbvrab  3439  mob2  3673  reu2  3683  reu6  3684  sbcralt  3822  sbcreu  3826  cbvrabcsfw  3890  cbvreucsf  3893  cbvrabcsf  3894  csbif  4537  cbvopab1  5172  cbvopab1g  5173  cbvopab1s  5175  cbvmptf  5198  cbvmptfg  5199  csbopab  5503  csbopabgALT  5504  opeliunxp  5691  opeliun2xp  5692  ralxpf  5795  cbviotaw  6455  cbviota  6457  csbiota  6485  f1ossf1o  7073  cbvriotaw  7324  cbvriota  7328  csbriota  7330  onminex  7747  tfis  7797  findes  7842  abrexex2g  7908  opabex3d  7909  opabex3rd  7910  opabex3  7911  dfoprab4f  8000  uzind4s  12821  ac6sf2  32700  esumcvg  34243  regsfromsetind  36669  wl-sb8t  37757  wl-sbalnae  37767  sbcrexgOLD  43027  scottabes  44483  pm13.193  44652  2reu8i  47359  ichnfimlem  47709