Theorem sbequ12 2263

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

Syntax hints:   → wi 4   ↔ wb 207  [wsb 2073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074

This theorem is referenced by:  sbequ12r  2264  sbequ12a  2266  sb8ef  2363  sbbib  2369  axc16ALT  2497  nfsb4t  2507  sbco2  2519  sb8  2525  sb8e  2526  sbal1  2536  sbal2  2537  sbab  2885  cbvrexsvw  3291  cbvralsvwOLD  3292  cbvralf  3324  cbvralsv  3330  cbvrexsv  3331  cbvrabwOLD  3427  cbvrab  3430  mob2  3656  reu2  3666  reu6  3667  sbcralt  3804  sbcreu  3808  cbvrabcsfw  3872  cbvreucsf  3875  cbvrabcsf  3876  csbif  4512  cbvopab1  5146  cbvopab1g  5147  cbvopab1s  5149  cbvmptf  5172  cbvmptfg  5173  csbopab  5497  csbopabgALT  5498  opeliunxp  5685  opeliun2xp  5686  ralxpf  5788  cbviotaw  6448  cbviota  6450  csbiota  6478  f1ossf1o  7070  cbvriotaw  7322  cbvriota  7326  csbriota  7328  onminex  7745  tfis  7795  findes  7840  abrexex2g  7906  opabex3d  7907  opabex3rd  7908  opabex3  7909  dfoprab4f  7998  uzind4s  12849  ac6sf2  32714  esumcvg  34270  regsfromsetind  36767  wl-sb8t  37923  wl-sbalnae  37933  scottabes  44686  pm13.193  44855  2reu8i  47576  ichnfimlem  47938