Theorem sbequ12 2289

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  [wsb 2099

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100

This theorem is used by:  sbequ12r  2290  sbequ12a  2292  sb8ef  2389  sbbib  2395  axc16ALT  2523  nfsb4t  2533  sbco2  2545  sb8  2551  sb8e  2552  sbal1  2562  sbal2  2563  sbab  2911  cbvrexsvw  3319  cbvralsvwOLD  3320  cbvralf  3351  cbvralsv  3357  cbvrexsv  3358  cbvrab  3456  mob2  3680  reu2  3690  reu6  3691  sbcralt  3826  sbcreu  3830  cbvrabcsfw  3895  cbvreucsf  3898  cbvrabcsf  3899  csbif  4547  cbvopab1  5187  cbvopab1g  5188  cbvopab1s  5190  cbvmptf  5213  cbvmptfg  5214  csbopab  5542  csbopabw  5543  opeliunxp  5730  opeliun2xp  5731  ralxpf  5834  cbviotaw  6503  cbviota  6505  csbiota  6533  f1ossf1o  7128  cbvriotaw  7382  cbvriota  7386  csbriota  7388  onminex  7803  tfis  7853  findes  7899  abrexex2g  7963  opabex3d  7964  opabex3rd  7965  opabex3  7966  dfoprab4f  8055  scottabes  9873  uzind4s  12944  ac6sf2  33014  esumcvg  34516  regsfromsetind  37083  wl-sb8t  38240  wl-sbalnae  38250  pm13.193  45154  2reu8i  47883  ichnfimlem  48245