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  2359  sbbib  2365  axc16ALT  2493  nfsb4t  2503  sbco2  2515  sb8  2521  sb8e  2522  sbal1  2532  sbal2  2533  sbab  2882  cbvrexsvw  3289  cbvralsvwOLD  3290  cbvralf  3322  cbvralsv  3328  cbvrexsv  3329  cbvrabwOLD  3425  cbvrab  3428  mob2  3661  reu2  3671  reu6  3672  sbcralt  3810  sbcreu  3814  cbvrabcsfw  3878  cbvreucsf  3881  cbvrabcsf  3882  csbif  4524  cbvopab1  5159  cbvopab1g  5160  cbvopab1s  5162  cbvmptf  5185  cbvmptfg  5186  csbopab  5510  csbopabgALT  5511  opeliunxp  5698  opeliun2xp  5699  ralxpf  5801  cbviotaw  6461  cbviota  6463  csbiota  6491  f1ossf1o  7081  cbvriotaw  7333  cbvriota  7337  csbriota  7339  onminex  7756  tfis  7806  findes  7851  abrexex2g  7917  opabex3d  7918  opabex3rd  7919  opabex3  7920  dfoprab4f  8009  uzind4s  12858  ac6sf2  32695  esumcvg  34230  regsfromsetind  36721  wl-sb8t  37877  wl-sbalnae  37887  scottabes  44669  pm13.193  44838  2reu8i  47561  ichnfimlem  47923