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 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  [wsb 2099

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2213

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100

This theorem is used by:  sbequ12r  2288  sbequ12a  2290  sb8ef  2385  sbbib  2391  axc16ALT  2519  nfsb4t  2529  sbco2  2541  sb8  2547  sb8e  2548  sbal1  2558  sbal2  2559  sbab  2907  cbvrexsvw  3315  cbvralf  3346  cbvralsv  3352  cbvrexsv  3353  cbvrab  3450  mob2  3673  reu2  3683  reu6  3684  sbcralt  3819  sbcreu  3823  cbvrabcsfw  3888  cbvreucsf  3891  cbvrabcsf  3892  csbif  4540  cbvopab1  5179  cbvopab1g  5180  cbvopab1s  5182  cbvmptf  5205  cbvmptfg  5206  csbopab  5530  csbopabw  5531  opeliunxp  5718  opeliun2xp  5719  ralxpf  5824  cbviotaw  6500  cbviota  6502  csbiota  6530  f1ossf1o  7127  cbvriotaw  7384  cbvriota  7388  csbriota  7390  onminex  7814  tfis  7864  findes  7910  abrexex2g  7974  opabex3d  7975  opabex3rd  7976  opabex3  7977  dfoprab4f  8065  scottabes  9934  uzind4s  13028  ac6sf2  33209  esumcvg  34711  regsfromsetind  37307  wl-sb8t  38464  wl-sbalnae  38474  pm13.193  45380  2reu8i  48152  ichnfimlem  48514