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  2879  cbvrexsvw  3285  cbvralsvwOLD  3286  cbvralsvwOLDOLD  3287  cbvrexsvwOLD  3288  cbvralf  3327  cbvralsv  3333  cbvrexsv  3334  cbvrabwOLD  3432  cbvrab  3436  mob2  3670  reu2  3680  reu6  3681  sbcralt  3819  sbcreu  3823  cbvrabcsfw  3887  cbvreucsf  3890  cbvrabcsf  3891  csbif  4534  cbvopab1  5169  cbvopab1g  5170  cbvopab1s  5172  cbvmptf  5195  cbvmptfg  5196  csbopab  5500  csbopabgALT  5501  opeliunxp  5688  opeliun2xp  5689  ralxpf  5792  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  12812  ac6sf2  32626  esumcvg  34171  wl-sb8t  37669  wl-sbalnae  37679  sbcrexgOLD  42942  scottabes  44399  pm13.193  44568  2reu8i  47275  ichnfimlem  47625