Theorem sbequ12 2254

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 2251	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑))
2		sbequ2 2252	. 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 2180

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

This theorem is referenced by:  sbequ12r  2255  sbequ12a  2257  sb8ef  2355  sbbib  2361  axc16ALT  2489  nfsb4t  2499  sbco2  2511  sb8  2517  sb8e  2518  sbal1  2528  sbal2  2529  sbab  2878  cbvrexsvw  3284  cbvralsvwOLD  3285  cbvralsvwOLDOLD  3286  cbvrexsvwOLD  3287  cbvralf  3326  cbvralsv  3332  cbvrexsv  3333  cbvrabwOLD  3431  cbvrab  3435  mob2  3669  reu2  3679  reu6  3680  sbcralt  3818  sbcreu  3822  cbvrabcsfw  3886  cbvreucsf  3889  cbvrabcsf  3890  csbif  4528  cbvopab1  5160  cbvopab1g  5161  cbvopab1s  5163  cbvmptf  5186  cbvmptfg  5187  csbopab  5490  csbopabgALT  5491  opeliunxp  5678  opeliun2xp  5679  ralxpf  5781  cbviotaw  6439  cbviota  6441  csbiota  6469  f1ossf1o  7056  cbvriotaw  7307  cbvriota  7311  csbriota  7313  onminex  7730  tfis  7780  findes  7825  abrexex2g  7891  opabex3d  7892  opabex3rd  7893  opabex3  7894  dfoprab4f  7983  uzind4s  12801  ac6sf2  32597  esumcvg  34091  wl-sb8t  37586  wl-sbalnae  37596  wl-ax11-lem8  37626  sbcrexgOLD  42818  scottabes  44275  pm13.193  44444  2reu8i  47144  ichnfimlem  47494