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

Theorem 3brtr4g 5183
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 5158 . 2 (𝐶𝑅𝐷𝐴𝑅𝐵)
51, 4sylibr 233 1 (𝜑𝐶𝑅𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542   class class class wbr 5149
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150
This theorem is referenced by:  eqbrtrid  5184  enrefnn  9047  enpr2dOLD  9050  limensuci  9153  infensuc  9155  djuen  10164  djudom1  10177  rlimneg  15593  isumsup2  15792  crth  16711  4sqlem6  16876  gzrngunit  21011  matgsum  21939  ovolunlem1a  25013  ovolfiniun  25018  ioombl1lem1  25075  ioombl1lem4  25078  iblss  25322  itgle  25327  dvfsumlem3  25545  emcllem6  26505  gausslemma2dlem0f  26864  gausslemma2dlem0g  26865  pntpbnd1a  27088  ostth2lem4  27139  noinfbnd2lem1  27233  omsmon  33297  itg2gt0cn  36543  dalem-cly  38542  dalem10  38544  fourierdlem103  44925  fourierdlem104  44926
  Copyright terms: Public domain W3C validator