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 234 1 (𝜑𝐶𝑅𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1539   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 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-br 5143
This theorem is referenced by:  eqbrtrid  5177  enrefnn  9088  enpr2dOLD  9091  limensuci  9194  infensuc  9196  djuen  10211  djudom1  10224  rlimneg  15684  isumsup2  15883  crth  16816  4sqlem6  16982  gzrngunit  21452  matgsum  22444  ovolunlem1a  25532  ovolfiniun  25537  ioombl1lem1  25594  ioombl1lem4  25597  iblss  25841  itgle  25846  dvfsumlem3  26070  emcllem6  27045  gausslemma2dlem0f  27406  gausslemma2dlem0g  27407  pntpbnd1a  27630  ostth2lem4  27681  noinfbnd2lem1  27776  omsmon  34301  itg2gt0cn  37683  dalem-cly  39674  dalem10  39676  fourierdlem103  46229  fourierdlem104  46230
  Copyright terms: Public domain W3C validator