Theorem eqbrtri 5100

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 5086	. 2 ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)
4	1, 3	mpbir 230	1 ⊢ 𝐴𝑅𝐶

Syntax hints:   = wceq 1542   class class class wbr 5079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-br 5080

This theorem is referenced by:  eqbrtrri  5102  3brtr4i  5109  infxpenc2  9779  dju1p1e2  9930  pwsdompw  9961  r1om  10001  aleph1  10328  canthp1lem1  10409  neg1lt0  12090  halflt1  12191  3halfnz  12399  declei  12472  numlti  12473  sqlecan  13923  discr  13953  faclbnd3  14004  hashunlei  14138  hashge2el2dif  14192  geo2lim  15585  0.999...  15591  geoihalfsum  15592  cos2bnd  15895  sin4lt0  15902  eirrlem  15911  rpnnen2lem3  15923  rpnnen2lem9  15929  aleph1re  15952  1nprm  16382  strle2  16858  strle3  16859  1strstr  16925  1strstr1  16926  2strstr  16932  2strstr1  16935  rngstr  17006  srngstr  17017  lmodstr  17033  ipsstr  17044  phlstr  17054  topgrpstr  17069  otpsstr  17084  odrngstr  17111  imasvalstr  17160  0frgp  19383  cnfldstr  20597  zlmlemOLD  20717  tnglemOLD  23795  iscmet3lem3  24452  mbfimaopnlem  24817  mbfsup  24826  mbfi1fseqlem6  24883  aalioulem3  25492  aaliou3lem3  25502  dvradcnv  25578  asin1  26042  log2cnv  26092  log2tlbnd  26093  mule1  26295  bposlem5  26434  bposlem8  26437  zabsle1  26442  trkgstr  26803  0pth  28485  ex-fl  28807  blocnilem  29162  norm3difi  29505  norm3adifii  29506  bcsiALT  29537  nmopsetn0  30223  nmfnsetn0  30236  nmopge0  30269  nmfnge0  30285  0bdop  30351  nmcexi  30384  opsqrlem6  30503  dp2lt10  31154  dplti  31175  dpmul4  31184  idlsrgstr  31643  locfinref  31787  dya2iocct  32243  signswch  32536  hgt750lem  32627  hgt750lem2  32628  subfaclim  33146  logi  33696  faclim  33708  cnndvlem1  34713  taupilem2  35489  cntotbnd  35950  60gcd7e1  40010  3lexlogpow5ineq1  40059  aks4d1p1p7  40079  acos1half  40167  diophren  40632  algstr  40999  pr2dom  41113  tr3dom  41114  binomcxplemnn0  41937  binomcxplemrat  41938  stirlinglem1  43586  dirkercncflem1  43615  fouriersw  43743  meaiunlelem  43977  nfermltl2rev  45164  evengpoap3  45220  exple2lt6  45669  nnlog2ge0lt1  45881