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

Theorem 3brtr4g 5144
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 5119 . 2 (𝐶𝑅𝐷𝐴𝑅𝐵)
51, 4sylibr 233 1 (𝜑𝐶𝑅𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542   class class class wbr 5110
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 2708
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 2715  df-cleq 2729  df-clel 2815  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111
This theorem is referenced by:  eqbrtrid  5145  enrefnn  8998  enpr2dOLD  9001  limensuci  9104  infensuc  9106  djuen  10112  djudom1  10125  rlimneg  15538  isumsup2  15738  crth  16657  4sqlem6  16822  gzrngunit  20879  matgsum  21802  ovolunlem1a  24876  ovolfiniun  24881  ioombl1lem1  24938  ioombl1lem4  24941  iblss  25185  itgle  25190  dvfsumlem3  25408  emcllem6  26366  gausslemma2dlem0f  26725  gausslemma2dlem0g  26726  pntpbnd1a  26949  ostth2lem4  27000  noinfbnd2lem1  27094  omsmon  32938  itg2gt0cn  36162  dalem-cly  38163  dalem10  38165  fourierdlem103  44524  fourierdlem104  44525
  Copyright terms: Public domain W3C validator