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

Theorem 3brtr4g 5176
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 5151 . 2 (𝐶𝑅𝐷𝐴𝑅𝐵)
51, 4sylibr 233 1 (𝜑𝐶𝑅𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541   class class class wbr 5142
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-br 5143
This theorem is referenced by:  eqbrtrid  5177  enrefnn  9032  enpr2dOLD  9035  limensuci  9138  infensuc  9140  djuen  10148  djudom1  10161  rlimneg  15577  isumsup2  15776  crth  16695  4sqlem6  16860  gzrngunit  20947  matgsum  21870  ovolunlem1a  24944  ovolfiniun  24949  ioombl1lem1  25006  ioombl1lem4  25009  iblss  25253  itgle  25258  dvfsumlem3  25476  emcllem6  26434  gausslemma2dlem0f  26793  gausslemma2dlem0g  26794  pntpbnd1a  27017  ostth2lem4  27068  noinfbnd2lem1  27162  omsmon  33192  itg2gt0cn  36411  dalem-cly  38411  dalem10  38413  fourierdlem103  44762  fourierdlem104  44763
  Copyright terms: Public domain W3C validator