Theorem sbequ12 2293

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

Syntax hints:   → wi 4   ↔ wb 209  [wsb 2097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098

This theorem is referenced by:  sbequ12r  2294  sbequ12a  2296  sb8ef  2393  sbbib  2399  axc16ALT  2527  nfsb4t  2537  sbco2  2549  sb8  2555  sb8e  2556  sbal1  2566  sbal2  2567  sbab  2915  cbvrexsvw  3323  cbvralsvwOLD  3324  cbvralf  3356  cbvralsv  3362  cbvrexsv  3363  cbvrabwOLD  3459  cbvrab  3462  mob2  3687  reu2  3697  reu6  3698  sbcralt  3834  sbcreu  3838  cbvrabcsfw  3902  cbvreucsf  3905  cbvrabcsf  3906  csbif  4547  cbvopab1  5186  cbvopab1g  5187  cbvopab1s  5189  cbvmptf  5212  cbvmptfg  5213  csbopab  5538  csbopabw  5539  opeliunxp  5726  opeliun2xp  5727  ralxpf  5830  cbviotaw  6497  cbviota  6499  csbiota  6527  f1ossf1o  7122  cbvriotaw  7374  cbvriota  7378  csbriota  7380  onminex  7797  tfis  7847  findes  7893  abrexex2g  7957  opabex3d  7958  opabex3rd  7959  opabex3  7960  dfoprab4f  8049  scottabes  9864  uzind4s  12928  ac6sf2  32904  esumcvg  34417  regsfromsetind  36935  wl-sb8t  38090  wl-sbalnae  38100  pm13.193  45008  2reu8i  47734  ichnfimlem  48096