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

Theorem 3brtr4g 4996
 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 4971 . 2 (𝐶𝑅𝐷𝐴𝑅𝐵)
51, 4sylibr 235 1 (𝜑𝐶𝑅𝐷)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1522   class class class wbr 4962 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-rab 3114  df-v 3439  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-br 4963 This theorem is referenced by:  eqbrtrid  4997  limensuci  8540  infensuc  8542  djuen  9441  djudom1  9454  rlimneg  14837  isumsup2  15034  crth  15944  4sqlem6  16108  gzrngunit  20293  matgsum  20730  ovolunlem1a  23780  ovolfiniun  23785  ioombl1lem1  23842  ioombl1lem4  23845  iblss  24088  itgle  24093  dvfsumlem3  24308  emcllem6  25260  gausslemma2dlem0f  25619  gausslemma2dlem0g  25620  pntpbnd1a  25843  ostth2lem4  25894  omsmon  31173  itg2gt0cn  34478  dalem-cly  36338  dalem10  36340  enpr2d  40051  fourierdlem103  42036  fourierdlem104  42037
 Copyright terms: Public domain W3C validator