Theorem sbequ12 2285

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

Syntax hints:   → wi 4   ↔ wb 208  [wsb 2089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-12 2211

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090

This theorem is referenced by:  sbequ12r  2286  sbequ12a  2288  sb8ef  2385  sbbib  2391  axc16ALT  2519  nfsb4t  2529  sbco2  2541  sb8  2547  sb8e  2548  sbal1  2558  sbal2  2559  sbab  2907  cbvrexsvw  3313  cbvralsvwOLD  3314  cbvralf  3346  cbvralsv  3352  cbvrexsv  3353  cbvrabwOLD  3449  cbvrab  3452  mob2  3676  reu2  3686  reu6  3687  sbcralt  3823  sbcreu  3827  cbvrabcsfw  3891  cbvreucsf  3894  cbvrabcsf  3895  csbif  4535  cbvopab1  5171  cbvopab1g  5172  cbvopab1s  5174  cbvmptf  5197  cbvmptfg  5198  csbopab  5522  csbopabw  5523  opeliunxp  5710  opeliun2xp  5711  ralxpf  5814  cbviotaw  6479  cbviota  6481  csbiota  6509  f1ossf1o  7105  cbvriotaw  7357  cbvriota  7361  csbriota  7363  onminex  7780  tfis  7830  findes  7876  abrexex2g  7940  opabex3d  7941  opabex3rd  7942  opabex3  7943  dfoprab4f  8032  uzind4s  12903  ac6sf2  32785  esumcvg  34344  regsfromsetind  36860  wl-sb8t  38016  wl-sbalnae  38026  scottabes  44779  pm13.193  44948  2reu8i  47668  ichnfimlem  48030