Theorem eqbrtri 5107

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)

Hypotheses

Ref	Expression
eqbrtr.1	⊢ 𝐴 = 𝐵
eqbrtr.2	⊢ 𝐵𝑅𝐶

Assertion

Ref	Expression
eqbrtri	⊢ 𝐴𝑅𝐶

Proof of Theorem eqbrtri

Step	Hyp	Ref	Expression
1		eqbrtr.2	. 2 ⊢ 𝐵𝑅𝐶
2		eqbrtr.1	. . 3 ⊢ 𝐴 = 𝐵
3	2	breq1i 5093	. 2 ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)
4	1, 3	mpbir 231	1 ⊢ 𝐴𝑅𝐶

Syntax hints:   = wceq 1542   class class class wbr 5086

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087

This theorem is referenced by:  eqbrtrri  5109  3brtr4i  5116  0sdom1dom  9147  1sdom2dom  9155  infxpenc2  9933  dju1p1e2  10085  pwsdompw  10114  r1om  10154  aleph1  10483  canthp1lem1  10564  halflt1  12359  3halfnz  12572  declei  12644  numlti  12645  sqlecan  14133  discr  14164  faclbnd3  14216  hashunlei  14349  hashge2el2dif  14404  geo2lim  15799  0.999...  15805  geoihalfsum  15806  cos2bnd  16114  sin4lt0  16121  eirrlem  16130  rpnnen2lem3  16142  rpnnen2lem9  16148  aleph1re  16171  1nprm  16607  strle2  17087  strle3  17088  1strstr  17151  2strstr  17155  rngstr  17219  srngstr  17230  lmodstr  17246  ipsstr  17257  phlstr  17267  topgrpstr  17282  otpsstr  17297  odrngstr  17324  imasvalstr  17372  chnub  18546  0frgp  19712  cnfldstr  21313  cnfldstrOLD  21328  iscmet3lem3  25235  mbfimaopnlem  25600  mbfsup  25609  mbfi1fseqlem6  25665  aalioulem3  26282  aaliou3lem3  26292  dvradcnv  26370  logi  26536  asin1  26844  log2cnv  26894  log2tlbnd  26895  mule1  27098  bposlem5  27239  bposlem8  27242  zabsle1  27247  trkgstr  28500  0pth  30184  ex-fl  30506  blocnilem  30864  norm3difi  31207  norm3adifii  31208  bcsiALT  31239  nmopsetn0  31925  nmfnsetn0  31938  nmopge0  31971  nmfnge0  31987  0bdop  32053  nmcexi  32086  opsqrlem6  32205  dp2lt10  32948  dplti  32969  dpmul4  32978  idlsrgstr  33567  locfinref  33991  dya2iocct  34430  signswch  34711  hgt750lem  34801  hgt750lem2  34802  subfaclim  35376  faclim  35934  cnndvlem1  36795  taupilem2  37634  cntotbnd  38108  60gcd7e1  42436  3lexlogpow5ineq1  42485  aks4d1p1p7  42505  acos1half  42789  diophren  43244  algstr  43604  pr2dom  43957  tr3dom  43958  binomcxplemnn0  44779  binomcxplemrat  44780  stirlinglem1  46506  dirkercncflem1  46535  fouriersw  46663  meaiunlelem  46900  nthrucw  47318  ceilhalf1  47768  nfermltl2rev  48177  evengpoap3  48233  exple2lt6  48798  nnlog2ge0lt1  49000  catbas  49659  cathomfval  49660  catcofval  49661