Theorem sbequ12 2229

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

Syntax hints:   → wi 4   ↔ wb 198  [wsb 2011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-12 2163

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-sb 2012

This theorem is referenced by:  sbequ12r  2230  sbequ12a  2231  sb8v  2321  sb8ev  2322  axc16ALT  2442  nfsb4t  2465  sbco2  2492  sb8  2501  sb8e  2502  sbal1  2539  clelab  2916  sbab  2918  cbvralf  3361  cbvralsv  3378  cbvrexsv  3379  cbvrab  3395  sbhypf  3455  mob2  3598  reu2  3606  reu6  3607  sbcralt  3728  sbcreu  3732  cbvreucsf  3785  cbvrabcsf  3786  csbif  4362  cbvopab1  4959  cbvopab1s  4961  cbvmptf  4983  cbvmpt  4984  opelopabsb  5222  csbopab  5245  csbopabgALT  5246  opeliunxp  5416  ralxpf  5514  cbviota  6104  csbiota  6128  f1ossf1o  6660  cbvriota  6893  csbriota  6895  onminex  7285  tfis  7332  findes  7374  abrexex2g  7422  opabex3d  7423  opabex3  7424  dfoprab4f  7505  uzind4s  12054  ac6sf2  29994  esumcvg  30746  bj-sbab  33361  wl-sb8t  33928  wl-sbalnae  33939  wl-ax11-lem8  33963  sbcrexgOLD  38309  pm13.193  39567  2reu8i  42154  opeliun2xp  43126