Theorem sbequ12 2259

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069

This theorem is referenced by:  sbequ12r  2260  sbequ12a  2262  sb8ef  2360  sbbib  2366  axc16ALT  2494  nfsb4t  2504  sbco2  2516  sb8  2522  sb8e  2523  sbal1  2533  sbal2  2534  sbab  2883  cbvrexsvw  3290  cbvralsvwOLD  3291  cbvralsvwOLDOLD  3292  cbvrexsvwOLD  3293  cbvralf  3332  cbvralsv  3338  cbvrexsv  3339  cbvrabwOLD  3437  cbvrab  3441  mob2  3675  reu2  3685  reu6  3686  sbcralt  3824  sbcreu  3828  cbvrabcsfw  3892  cbvreucsf  3895  cbvrabcsf  3896  csbif  4539  cbvopab1  5174  cbvopab1g  5175  cbvopab1s  5177  cbvmptf  5200  cbvmptfg  5201  csbopab  5511  csbopabgALT  5512  opeliunxp  5699  opeliun2xp  5700  ralxpf  5803  cbviotaw  6463  cbviota  6465  csbiota  6493  f1ossf1o  7083  cbvriotaw  7334  cbvriota  7338  csbriota  7340  onminex  7757  tfis  7807  findes  7852  abrexex2g  7918  opabex3d  7919  opabex3rd  7920  opabex3  7921  dfoprab4f  8010  uzind4s  12833  ac6sf2  32711  esumcvg  34263  regsfromsetind  36688  wl-sb8t  37804  wl-sbalnae  37814  sbcrexgOLD  43139  scottabes  44595  pm13.193  44764  2reu8i  47470  ichnfimlem  47820