Theorem sbequ12 2287

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097

This theorem is referenced by:  sbequ12r  2288  sbequ12a  2290  sb8ef  2387  sbbib  2393  axc16ALT  2521  nfsb4t  2531  sbco2  2543  sb8  2549  sb8e  2550  sbal1  2560  sbal2  2561  sbab  2909  cbvrexsvw  3317  cbvralsvwOLD  3318  cbvralf  3349  cbvralsv  3355  cbvrexsv  3356  cbvrab  3454  mob2  3678  reu2  3688  reu6  3689  sbcralt  3825  sbcreu  3829  cbvrabcsfw  3894  cbvreucsf  3897  cbvrabcsf  3898  csbif  4545  cbvopab1  5185  cbvopab1g  5186  cbvopab1s  5188  cbvmptf  5211  cbvmptfg  5212  csbopab  5540  csbopabw  5541  opeliunxp  5728  opeliun2xp  5729  ralxpf  5832  cbviotaw  6499  cbviota  6501  csbiota  6529  f1ossf1o  7124  cbvriotaw  7376  cbvriota  7380  csbriota  7382  onminex  7797  tfis  7847  findes  7893  abrexex2g  7957  opabex3d  7958  opabex3rd  7959  opabex3  7960  dfoprab4f  8049  scottabes  9864  uzind4s  12927  ac6sf2  32967  esumcvg  34476  regsfromsetind  37050  wl-sb8t  38207  wl-sbalnae  38217  pm13.193  45121  2reu8i  47850  ichnfimlem  48212