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

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

Proof of Theorem sbequ12
StepHypRef Expression
1 sbequ1 2248 . 2 (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑))
2 sbequ2 2249 . 2 (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑𝜑))
31, 2impbid 212 1 (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  [wsb 2064
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-12 2177
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065
This theorem is referenced by:  sbequ12r  2252  sbequ12a  2254  sb8fOLD  2357  sb8ef  2358  sbbib  2364  axc16ALT  2494  nfsb4t  2504  sbco2  2516  sb8  2522  sb8e  2523  sbal1  2533  sbal2  2534  sbab  2889  cbvrexsvw  3318  cbvralsvwOLD  3319  cbvralsvwOLDOLD  3320  cbvrexsvwOLD  3321  cbvralf  3360  cbvralsv  3366  cbvrexsv  3367  cbvrabwOLD  3474  cbvrab  3479  sbhypfOLD  3545  mob2  3721  reu2  3731  reu6  3732  sbcralt  3872  sbcreu  3876  cbvrabcsfw  3940  cbvreucsf  3943  cbvrabcsf  3944  csbif  4583  cbvopab1  5217  cbvopab1g  5218  cbvopab1s  5220  cbvmptf  5251  cbvmptfg  5252  csbopab  5560  csbopabgALT  5561  opeliunxp  5752  opeliun2xp  5753  ralxpf  5857  cbviotaw  6521  cbviota  6523  csbiota  6554  f1ossf1o  7148  cbvriotaw  7397  cbvriota  7401  csbriota  7403  onminex  7822  tfis  7876  findes  7922  abrexex2g  7989  opabex3d  7990  opabex3rd  7991  opabex3  7992  dfoprab4f  8081  uzind4s  12950  ac6sf2  32634  esumcvg  34087  wl-sb8t  37553  wl-sbalnae  37563  wl-ax11-lem8  37593  sbcrexgOLD  42796  scottabes  44261  pm13.193  44430  2reu8i  47125  ichnfimlem  47450
  Copyright terms: Public domain W3C validator