Theorem eqbrtrrd 5128

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

Hypotheses

Ref	Expression
eqbrtrrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqbrtrrd.2	⊢ (𝜑 → 𝐴𝑅𝐶)

Assertion

Ref	Expression
eqbrtrrd	⊢ (𝜑 → 𝐵𝑅𝐶)

Proof of Theorem eqbrtrrd

Step	Hyp	Ref	Expression
1		eqbrtrrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	eqcomd 2766	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqbrtrrd.2	. 2 ⊢ (𝜑 → 𝐴𝑅𝐶)
4	2, 3	eqbrtrd 5126	1 ⊢ (𝜑 → 𝐵𝑅𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103

This theorem is used by:  dftpos4  8270  dif1en  9185  fodomfi  9312  fmptssfisupp  9393  cnfcom2lem  9709  dmttrcl  9729  ttrclselem2  9734  ficardadju  10285  enfin1ai  10469  pwcfsdom  10675  fpwwe2lem6  10728  fpwwe2  10735  canthp1lem1  10744  1nqenq  11054  prlem936  11139  lemulge11  12186  supaddc  12291  supmul1  12293  mul2lt0llt0  13233  mul2lt0lgt0  13234  xaddge0  13395  xadddi2  13434  ltexp2a  14316  leexp2a  14322  nnlesq  14356  digit1  14388  faclbnd4lem1  14444  faclbnd6  14450  facavg  14452  prsshashgt1  14562  nehash2  14626  sgnmulsgn  15271  abs3dif  15508  abs2dif  15509  limsupgre  15657  rlimclim1  15721  rlimuni  15726  rlimres2  15737  rlimcn1  15764  rlimcn1b  15765  recn2  15777  imcn2  15778  rlimo1  15793  o1rlimmul  15795  iserex  15833  isercoll  15844  caucvgrlem2  15851  caucvgr  15852  iseraltlem3  15860  summolem2a  15890  fsumge1  15973  o1fsum  15989  isumrpcl  16021  climcnds  16029  harmonic  16037  mertenslem1  16062  prodmolem2a  16110  ege2le3  16265  efgt1p2  16291  efgt1p  16292  eirrlem  16381  rpnnen2lem11  16401  fsumdvds  16487  bitsfzo  16614  bitsmod  16615  bitscmp  16617  mulgcd  16730  dvdsexpnn  16749  nn0seqcvgd  16754  mulgcddvds  16839  rpdvds  16844  qden1elz  16942  phimullem  16965  hashgcdlem  16974  hashgcdeq  16976  pcdvdstr  17063  pockthg  17093  prmreclem1  17103  4sqlem11  17142  ramub1lem1  17213  ramub1lem2  17214  mreexexlem4d  17830  sscid  18008  latmlej21  18663  latmlej22  18664  lubel  18697  efginvrel1  19951  odadd2  20072  odadd  20073  gexexlem  20075  cyggex2  20120  ablfacrplem  20290  ablfac1c  20296  ablfac1eu  20298  pgpfac1lem3a  20301  isabvd  21078  ornglmulle  21133  orngrmulle  21134  mptscmfsuppd  21212  znrrg  21880  frlmphl  22096  frlmup1  22113  f1linds  22140  selvvvval  22460  psdmplcl  22492  chcoeffeqlem  23212  lmcn2  23977  metrtri  24685  imasdsf1olem  24701  stdbdxmet  24843  nrmmetd  24902  nmmtri  24950  nlmvscnlem2  25013  blcvx  25126  recld2  25143  zdis  25145  opnreen  25160  cnheibor  25285  lebnumlem3  25293  nmoleub2lem3  25445  nmoleub2lem2  25446  nmoleub3  25449  ipcnlem2  25574  cmetcaulem  25618  nglmle  25632  cncmet  25652  csbren  25729  trirn  25730  minveclem4  25762  ovoliunlem1  25832  ovoliun2  25836  ovolscalem1  25843  ovolicopnf  25854  voliunlem2  25881  volsup  25886  ioorcl2  25902  uniiccvol  25910  uniioombllem4  25916  i1fd  26011  mbfi1fseqlem4  26048  itg2const2  26071  itg2eqa  26075  itg2split  26079  itg2i1fseqle  26084  itg2cnlem2  26092  dvcnv  26306  dveflem  26308  dvferm1lem  26313  dvlip2  26324  c1liplem1  26325  dvivthlem1  26337  lhop1lem  26342  dvcvx  26349  dvfsumle  26350  dvfsumabs  26352  dvfsumlem4  26358  dvfsumrlim2  26361  ftc1a  26366  tdeglem4  26387  deg1pwle  26447  fta1blem  26498  aalioulem3  26670  aaliou2b  26677  ulmbdd  26734  ulmdvlem1  26736  itgulm  26744  pserdvlem2  26764  abelthlem3  26769  abelthlem5  26771  abelthlem6  26772  abelthlem7  26774  tanregt0  26876  argimlt0  26950  logdivlti  26957  logcnlem3  26981  logcnlem4  26982  logtayl  26997  logtayl2  26999  cxple2  27034  cxpcn3lem  27084  cxpaddle  27089  rtprmirr  27097  isosctrlem1  27155  atantayl  27274  efrlim  27306  dfef2  27307  o1cxp  27311  cxp2lim  27313  divsqrtsumo1  27320  amgmlem  27326  logdifbnd  27330  emcllem7  27338  harmonicbnd4  27347  fsumharmonic  27348  lgamgulmlem2  27366  lgamgulmlem3  27367  lgamucov  27374  lgamcvg2  27391  gamcvg2  27396  ftalem2  27410  basellem2  27418  basellem5  27421  basellem9  27425  vma1  27502  sqff1o  27518  fsumfldivdiaglem  27525  chtub  27548  fsumvma2  27550  chpchtsum  27555  chpub  27556  logfaclbnd  27558  logfacbnd3  27559  logfacrlim  27560  logexprlim  27561  bcmono  27613  bposlem2  27621  bposlem5  27624  bposlem6  27625  lgsne0  27671  lgsquadlem1  27716  lgsquadlem2  27717  2sqblem  27767  2sqmod  27772  chebbnd1lem1  27805  chtppilimlem1  27809  chtppilimlem2  27810  chpchtlim  27815  rplogsumlem1  27820  dchrvmasumiflem1  27837  dchrisum0flblem2  27845  dchrisum0fno1  27847  dchrisum0lem2a  27853  dchrisum0lem3  27855  dirith  27865  mulog2sumlem1  27870  mulog2sumlem2  27871  log2sumbnd  27880  selberglem2  27882  logdivbnd  27892  selberg3lem1  27893  selberg4lem1  27896  pntrsumbnd2  27903  pntrlog2bndlem1  27913  pntrlog2bndlem5  27917  pntrlog2bndlem6  27919  pntpbnd1a  27921  pntpbnd1  27922  pntpbnd2  27923  pntibndlem3  27928  pntlemb  27933  pntlemn  27936  pntlemr  27938  pntlemj  27939  pntlemf  27941  pntlemo  27943  ostth2lem3  27971  ostth3  27974  addsuniflem  28396  ltsp1d  28410  negsid  28436  negsunif  28450  negleft  28453  mulsuniflem  28544  precsexlem9  28610  n0sge0  28733  zcuts  28802  halfcut  28853  addhalfcut  28854  pw2cut2  28857  bdayfinbndlem1  28862  footeq  29208  hlperpnel  29210  perpdragALT  29212  perpdrag  29213  colperp  29214  mideulem2  29219  opphllem  29220  opphllem3  29234  lmieu  29298  trgcopy  29320  sacgr  29348  acopyeu  29351  perpeqlem  29356  angmgmaddcpbl  29399  perpprlng  29437  prlngmid2  29448  usgredgleordALT  29824  pthhashvtx  30324  eucrctshift  30853  nvabs  31283  smcnlem  31308  ubthlem2  31482  minvecolem4  31491  htthlem  31528  normpyc  31757  nmophmi  32642  hstle  32841  hstles  32842  stlei  32851  f1rnen  33273  nnmulge  33381  fsumiunle  33470  wrdt2ind  33566  xrge0npcan  33631  gsumwrd2dccat  33689  trsp2cyc  33734  archirngz  33800  archiabllem1a  33802  archiabllem2a  33805  archiabllem2c  33806  elrgspnlem1  33853  elrgspn  33857  elrgspnsubrunlem2  33859  rprmasso  34107  q1pdir  34185  r1pquslmic  34192  selvply1rhmlema  34200  selvply1rhmlem1  34202  evlextv  34224  mplvrpmga  34227  mplvrpmrhm  34229  drngdimgt0  34300  lbsdiflsp0  34308  fldextrspundgle  34360  fldext2rspun  34364  minplyirredlem  34392  madjusmdetlem2  34510  esumpinfval  34755  esumpinfsum  34759  esumpcvgval  34760  esum2d  34775  esumiun  34776  dya2icoseg  34959  omssubadd  34982  carsgsigalem  34997  carsggect  35000  carsgclctunlem3  35002  omsmeas  35005  eulerpartlems  35042  signsplypnf  35229  signsply0  35230  reprlt  35298  reprinfz1  35301  hgt750lemc  35326  hgt750lemf  35332  resconn  36129  sinccvglem  36555  circum  36557  btwnxfr  36945  nn0prpwlem  37234  dnibndlem2  37469  unblimceq0  37497  irrdiff  38384  poimirlem7  38682  mblfinlem3  38714  mblfinlem4  38715  itg2addnclem3  38728  ftc1anc  38756  isbnd3  38855  cntotbnd  38867  bfp  38895  rrndstprj2  38902  1cvrjat  40669  3atlem1  40677  3atlem6  40682  llnmlplnN  40733  2llnjaN  40760  2lplnja  40813  dalem57  40923  dalawlem11  41075  dalawlem12  41076  lhp2lt  41195  lhpj1  41216  lhpm0atN  41223  4atexlemex2  41265  lautm  41288  cdleme17b  41481  cdleme20j  41512  cdleme30a  41572  cdlemg4c  41806  cdlemg17a  41855  cdlemg31c  41893  trljco  41934  cdlemk46  42142  dia2dimlem2  42259  cdlemm10N  42312  cdlemn10  42400  dihmeetlem1N  42484  dihglblem5apreN  42485  dihmeetlem15N  42515  mapdat  42861  lcmineqlem19  43234  lcmineqlem20  43235  aks4d1p1p5  43262  aks4d1p8d2  43272  aks4d1p8  43274  aks4d1p9  43275  hashscontpow  43309  mullt0b1d  43684  evlselv  43754  mhphflem  43761  fltnlta  43811  3cubeslem1  43831  irrapxlem1  43966  irrapxlem4  43969  pell1qrgaplem  44017  pellfundglb  44029  rmspecfund  44053  monotoddzzfi  44086  rmynn  44100  jm2.24nn  44103  jm2.17c  44106  jm2.24  44107  acongeq  44127  jm2.20nn  44141  jm2.26lem3  44145  jm2.27a  44149  jm2.27c  44151  rmydioph  44158  jm3.1lem2  44162  frlmpwfi  44237  areaquad  44355  cantnf2  44464  rp-isfinite6  44656  frege129d  44900  leeq1d  45294  imo72b2lem0  45302  imo72b2  45309  cvgdvgrat  45434  radcnvrat  45435  hashnzfzclim  45443  isosctrlem1ALT  46052  cncmpmax  46185  iooabslt  46647  fmul01lt1lem2  46733  clim1fr1  46749  limcrecl  46777  climxrrelem  46895  liminflbuz2  46961  dvnprodlem1  47092  stoweidlem1  47147  stoweidlem11  47157  stoweidlem14  47160  stoweidlem24  47170  stoweidlem26  47172  wallispilem4  47214  wallispilem5  47215  stirlinglem1  47220  fourierdlem51  47303  fourierdlem65  47317  fouriersw  47377  2leaddle2  48504  2timesltsqm1  48585  sqrtpwpw2p  48759  lighneallem4a  48829  flnn0div2ge  49781  logbpw2m1  49815  functermclem  50778  amgmwlem  51198