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 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  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  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  5534  csbopabw  5535  opeliunxp  5722  opeliun2xp  5723  ralxpf  5826  cbviotaw  6496  cbviota  6498  csbiota  6526  f1ossf1o  7122  cbvriotaw  7379  cbvriota  7383  csbriota  7385  onminex  7801  tfis  7851  findes  7897  abrexex2g  7961  opabex3d  7962  opabex3rd  7963  opabex3  7964  dfoprab4f  8053  scottabes  9880  uzind4s  12957  ac6sf2  33095  esumcvg  34596  regsfromsetind  37158  wl-sb8t  38315  wl-sbalnae  38325  pm13.193  45235  2reu8i  48001  ichnfimlem  48363