Theorem sbequ12 2256

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

Syntax hints:   → wi 4   ↔ wb 206  [wsb 2067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2182

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068

This theorem is referenced by:  sbequ12r  2257  sbequ12a  2259  sb8ef  2357  sbbib  2363  axc16ALT  2491  nfsb4t  2501  sbco2  2513  sb8  2519  sb8e  2520  sbal1  2530  sbal2  2531  sbab  2880  cbvrexsvw  3286  cbvralsvwOLD  3287  cbvralsvwOLDOLD  3288  cbvrexsvwOLD  3289  cbvralf  3328  cbvralsv  3334  cbvrexsv  3335  cbvrabwOLD  3433  cbvrab  3437  mob2  3671  reu2  3681  reu6  3682  sbcralt  3820  sbcreu  3824  cbvrabcsfw  3888  cbvreucsf  3891  cbvrabcsf  3892  csbif  4534  cbvopab1  5169  cbvopab1g  5170  cbvopab1s  5172  cbvmptf  5195  cbvmptfg  5196  csbopab  5500  csbopabgALT  5501  opeliunxp  5688  opeliun2xp  5689  ralxpf  5793  cbviotaw  6452  cbviota  6454  csbiota  6482  f1ossf1o  7070  cbvriotaw  7321  cbvriota  7325  csbriota  7327  onminex  7744  tfis  7794  findes  7839  abrexex2g  7905  opabex3d  7906  opabex3rd  7907  opabex3  7908  dfoprab4f  7997  uzind4s  12816  ac6sf2  32616  esumcvg  34110  wl-sb8t  37607  wl-sbalnae  37617  sbcrexgOLD  42892  scottabes  44349  pm13.193  44518  2reu8i  47227  ichnfimlem  47577