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

Theorem 3brtr4g 5065
 Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.)
Hypotheses
Ref Expression
3brtr4g.1 (𝜑𝐴𝑅𝐵)
3brtr4g.2 𝐶 = 𝐴
3brtr4g.3 𝐷 = 𝐵
Assertion
Ref Expression
3brtr4g (𝜑𝐶𝑅𝐷)

Proof of Theorem 3brtr4g
StepHypRef Expression
1 3brtr4g.1 . 2 (𝜑𝐴𝑅𝐵)
2 3brtr4g.2 . . 3 𝐶 = 𝐴
3 3brtr4g.3 . . 3 𝐷 = 𝐵
42, 3breq12i 5040 . 2 (𝐶𝑅𝐷𝐴𝑅𝐵)
51, 4sylibr 237 1 (𝜑𝐶𝑅𝐷)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   class class class wbr 5031 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-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5032 This theorem is referenced by:  eqbrtrid  5066  enpr2d  8583  limensuci  8680  infensuc  8682  djuen  9583  djudom1  9596  rlimneg  14998  isumsup2  15196  crth  16108  4sqlem6  16272  gzrngunit  20161  matgsum  21052  ovolunlem1a  24110  ovolfiniun  24115  ioombl1lem1  24172  ioombl1lem4  24175  iblss  24418  itgle  24423  dvfsumlem3  24641  emcllem6  25596  gausslemma2dlem0f  25955  gausslemma2dlem0g  25956  pntpbnd1a  26179  ostth2lem4  26230  omsmon  31681  itg2gt0cn  35131  dalem-cly  36986  dalem10  36988  fourierdlem103  42894  fourierdlem104  42895
 Copyright terms: Public domain W3C validator