MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbequ12 Structured version   Visualization version   GIF version

Theorem sbequ12 2243
Description: An equality theorem for substitution. (Contributed by NM, 14-May-1993.)
Assertion
Ref Expression
sbequ12 (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))

Proof of Theorem sbequ12
StepHypRef Expression
1 sbequ1 2239 . 2 (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑))
2 sbequ2 2240 . 2 (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑𝜑))
31, 2impbid 213 1 (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  [wsb 2060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-12 2167
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061
This theorem is referenced by:  sbequ12r  2244  sbequ12a  2246  sb5  2267  sb8v  2364  sb8ev  2365  sbbib  2371  axc16ALT  2521  nfsb4t  2532  sbco2  2546  sb8  2552  sb8e  2553  sbal1  2565  sbal2  2566  clelab  2955  sbab  2957  nfabdw  2997  cbvralfw  3435  cbvralf  3437  cbvralsvw  3465  cbvrexsvw  3466  cbvralsv  3467  cbvrexsv  3468  cbvrabw  3487  cbvrab  3488  sbhypf  3550  mob2  3703  reu2  3713  reu6  3714  sbcralt  3852  sbcreu  3856  cbvrabcsfw  3921  cbvreucsf  3924  cbvrabcsf  3925  csbif  4518  cbvopab1  5130  cbvopab1g  5131  cbvopab1s  5133  cbvmptf  5156  cbvmptfg  5157  opelopabsb  5408  csbopab  5433  csbopabgALT  5434  opeliunxp  5612  ralxpf  5710  cbviotaw  6314  cbviota  6316  csbiota  6341  f1ossf1o  6882  cbvriotaw  7112  cbvriota  7116  csbriota  7118  onminex  7511  tfis  7558  findes  7601  abrexex2g  7654  opabex3d  7655  opabex3rd  7656  opabex3  7657  dfoprab4f  7743  uzind4s  12296  ac6sf2  30298  esumcvg  31244  wl-sb8t  34669  wl-sbalnae  34679  wl-ax11-lem8  34705  sbcrexgOLD  39260  scottabes  40455  pm13.193  40620  2reu8i  43189  opeliun2xp  44309
  Copyright terms: Public domain W3C validator