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

Theorem 3brtr4i 5140
Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.)
Hypotheses
Ref Expression
3brtr4.1 𝐴𝑅𝐵
3brtr4.2 𝐶 = 𝐴
3brtr4.3 𝐷 = 𝐵
Assertion
Ref Expression
3brtr4i 𝐶𝑅𝐷

Proof of Theorem 3brtr4i
StepHypRef Expression
1 3brtr4.2 . . 3 𝐶 = 𝐴
2 3brtr4.1 . . 3 𝐴𝑅𝐵
31, 2eqbrtri 5131 . 2 𝐶𝑅𝐵
4 3brtr4.3 . 2 𝐷 = 𝐵
53, 4breqtrri 5137 1 𝐶𝑅𝐷
Colors of variables: wff setvar class
Syntax hints:   = 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:  1lt2nq  10916  0lt1sr  11038  declt  12653  decltc  12654  decle  12659  fzennn  13880  faclbnd4lem1  14200  fsumabs  15693  basendxltplusgndx  17169  basendxlttsetndx  17243  basendxltplendx  17257  basendxltdsndx  17276  basendxltunifndx  17286  ovolfiniun  24881  log2ublem3  26314  log2ub  26315  bclbnd  26644  bposlem8  26655  basendxltedgfndx  27986  baseltedgfOLD  27987  nmblolbii  29783  normlem6  30099  norm-ii-i  30121  nmbdoplbi  31008  dp2lt  31783  dp2ltsuc  31784  dp2ltc  31785  dplt  31802  dpltc  31805  dpmul4  31812  hgt750lemd  33301  hgt750lem  33304  supxrltinfxr  43758  nnsum4primesevenALTV  46067
  Copyright terms: Public domain W3C validator