Theorem sbequ12 2290

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 2287	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑))
2		sbequ2 2288	. 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  2291  sbequ12a  2293  sb8ef  2390  sbbib  2396  axc16ALT  2524  nfsb4t  2534  sbco2  2546  sb8  2552  sb8e  2553  sbal1  2563  sbal2  2564  sbab  2912  cbvrexsvw  3320  cbvralsvwOLD  3321  cbvralf  3352  cbvralsv  3358  cbvrexsv  3359  cbvrab  3457  mob2  3681  reu2  3691  reu6  3692  sbcralt  3828  sbcreu  3832  cbvrabcsfw  3897  cbvreucsf  3900  cbvrabcsf  3901  csbif  4548  cbvopab1  5188  cbvopab1g  5189  cbvopab1s  5191  cbvmptf  5214  cbvmptfg  5215  csbopab  5543  csbopabw  5544  opeliunxp  5731  opeliun2xp  5732  ralxpf  5835  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  9872  uzind4s  12942  ac6sf2  32982  esumcvg  34489  regsfromsetind  37082  wl-sb8t  38239  wl-sbalnae  38249  pm13.193  45153  2reu8i  47882  ichnfimlem  48244