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

Theorem sbequ12r 2251
 Description: An equality theorem for substitution. (Contributed by NM, 6-Oct-2004.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
Assertion
Ref Expression
sbequ12r (𝑥 = 𝑦 → ([𝑥 / 𝑦]𝜑𝜑))

Proof of Theorem sbequ12r
StepHypRef Expression
1 sbequ12 2250 . . 3 (𝑦 = 𝑥 → (𝜑 ↔ [𝑥 / 𝑦]𝜑))
21bicomd 226 . 2 (𝑦 = 𝑥 → ([𝑥 / 𝑦]𝜑𝜑))
32equcoms 2027 1 (𝑥 = 𝑦 → ([𝑥 / 𝑦]𝜑𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209  [wsb 2069 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2175 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070 This theorem is referenced by:  sbelx  2252  sbequ12a  2253  sbid  2254  sbid2vw  2257  sb6rfv  2365  sbbib  2369  sb5rf  2479  sb6rf  2480  2sb5rf  2485  2sb6rf  2486  abbi  2865  opeliunxp  5587  isarep1  6420  findes  7606  axrepndlem1  10021  axrepndlem2  10022  nn0min  30606  esumcvg  31521  bj-sbidmOLD  34440  wl-nfs1t  35093  wl-sb6rft  35100  wl-equsb4  35109  wl-ax11-lem5  35137  sbcalf  35703  sbcexf  35704  opeliun2xp  44902
 Copyright terms: Public domain W3C validator