Theorem sbequ12 2286

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099

This theorem is used by:  sbequ12r  2287  sbequ12a  2289  sb8ef  2384  sbbib  2390  axc16ALT  2518  nfsb4t  2528  sbco2  2540  sb8  2546  sb8e  2547  sbal1  2557  sbal2  2558  sbab  2906  cbvrexsvw  3314  cbvralf  3345  cbvralsv  3351  cbvrexsv  3352  cbvrab  3449  mob2  3672  reu2  3682  reu6  3683  sbcralt  3819  sbcreu  3823  cbvrabcsfw  3888  cbvreucsf  3891  cbvrabcsf  3892  csbif  4539  cbvopab1  5178  cbvopab1g  5179  cbvopab1s  5181  cbvmptf  5204  cbvmptfg  5205  csbopab  5529  csbopabw  5530  opeliunxp  5717  opeliun2xp  5718  ralxpf  5824  cbviotaw  6503  cbviota  6505  csbiota  6534  f1ossf1o  7132  cbvriotaw  7388  cbvriota  7392  csbriota  7394  onminex  7818  tfis  7868  findes  7914  abrexex2g  7978  opabex3d  7979  opabex3rd  7980  opabex3  7981  dfoprab4f  8069  scottabes  9946  uzind4s  13040  ac6sf2  33265  esumcvg  34766  reu6f  35757  regsfromsetind  37421  wl-sb8t  38591  wl-sbalnae  38601  pm13.193  45502  2reu8i  48290  ichnfimlem  48652