Theorem eqbrtrrd 5109

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 2742	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqbrtrrd.2	. 2 ⊢ (𝜑 → 𝐴𝑅𝐶)
4	2, 3	eqbrtrd 5107	1 ⊢ (𝜑 → 𝐵𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5085

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086

This theorem is referenced by:  dftpos4  8195  dif1en  9096  fodomfi  9222  fodomfiOLD  9240  fmptssfisupp  9307  resfifsupp  9310  cnfcom2lem  9622  dmttrcl  9642  ttrclselem2  9647  ficardadju  10122  enfin1ai  10306  pwcfsdom  10506  fpwwe2lem6  10559  fpwwe2  10566  canthp1lem1  10575  1nqenq  10885  prlem936  10970  lemulge11  12018  supaddc  12123  supmul1  12125  mul2lt0llt0  13048  mul2lt0lgt0  13049  xaddge0  13210  xadddi2  13249  ltexp2a  14128  leexp2a  14134  nnlesq  14167  digit1  14199  faclbnd4lem1  14255  faclbnd6  14261  facavg  14263  prsshashgt1  14372  nehash2  14436  abs3dif  15294  abs2dif  15295  limsupgre  15443  rlimclim1  15507  rlimuni  15512  rlimres2  15523  rlimcn1  15550  rlimcn1b  15551  recn2  15563  imcn2  15564  rlimo1  15579  o1rlimmul  15581  iserex  15619  isercoll  15630  caucvgrlem2  15637  caucvgr  15638  iseraltlem3  15646  summolem2a  15677  fsumge1  15760  o1fsum  15776  isumrpcl  15808  climcnds  15816  harmonic  15824  mertenslem1  15849  prodmolem2a  15899  ege2le3  16055  efgt1p2  16081  efgt1p  16082  eirrlem  16171  rpnnen2lem11  16191  fsumdvds  16277  bitsfzo  16404  bitsmod  16405  bitscmp  16407  mulgcd  16517  dvdssqlem  16535  nn0seqcvgd  16539  mulgcddvds  16624  rpdvds  16629  qden1elz  16727  phimullem  16749  hashgcdlem  16758  hashgcdeq  16760  pcdvdstr  16847  pockthg  16877  prmreclem1  16887  4sqlem11  16926  ramub1lem1  16997  ramub1lem2  16998  mreexexlem4d  17613  sscid  17791  latmlej21  18446  latmlej22  18447  lubel  18480  efginvrel1  19703  odadd2  19824  odadd  19825  gexexlem  19827  cyggex2  19872  ablfacrplem  20042  ablfac1c  20048  ablfac1eu  20050  pgpfac1lem3a  20053  isabvd  20789  ornglmulle  20844  orngrmulle  20845  mptscmfsuppd  20923  znrrg  21545  frlmphl  21761  frlmup1  21778  f1linds  21805  psdmplcl  22128  chcoeffeqlem  22850  lmcn2  23614  metrtri  24322  imasdsf1olem  24338  stdbdxmet  24480  nrmmetd  24539  nmmtri  24587  nlmvscnlem2  24650  blcvx  24763  recld2  24780  zdis  24782  opnreen  24797  cnheibor  24922  lebnumlem3  24930  nmoleub2lem3  25082  nmoleub2lem2  25083  nmoleub3  25086  ipcnlem2  25211  cmetcaulem  25255  nglmle  25269  cncmet  25289  csbren  25366  trirn  25367  minveclem4  25399  ovoliunlem1  25469  ovoliun2  25473  ovolscalem1  25480  ovolicopnf  25491  voliunlem2  25518  volsup  25523  ioorcl2  25539  uniiccvol  25547  uniioombllem4  25553  i1fd  25648  mbfi1fseqlem4  25685  itg2const2  25708  itg2eqa  25712  itg2split  25716  itg2i1fseqle  25721  itg2cnlem2  25729  dvcnv  25944  dveflem  25946  dvferm1lem  25951  dvlip2  25962  c1liplem1  25963  dvivthlem1  25975  lhop1lem  25980  dvcvx  25987  dvfsumle  25988  dvfsumabs  25990  dvfsumlem4  25996  dvfsumrlim2  25999  ftc1a  26004  tdeglem4  26025  deg1pwle  26085  fta1blem  26136  aalioulem3  26300  aaliou2b  26307  ulmbdd  26363  ulmdvlem1  26365  itgulm  26373  pserdvlem2  26393  abelthlem3  26398  abelthlem5  26400  abelthlem6  26401  abelthlem7  26403  tanregt0  26503  argimlt0  26577  logdivlti  26584  logcnlem3  26608  logcnlem4  26609  logtayl  26624  logtayl2  26626  cxple2  26661  cxpcn3lem  26711  cxpaddle  26716  rtprmirr  26724  isosctrlem1  26782  atantayl  26901  efrlim  26933  dfef2  26934  o1cxp  26938  cxp2lim  26940  divsqrtsumo1  26947  amgmlem  26953  logdifbnd  26957  emcllem7  26965  harmonicbnd4  26974  fsumharmonic  26975  lgamgulmlem2  26993  lgamgulmlem3  26994  lgamucov  27001  lgamcvg2  27018  gamcvg2  27023  ftalem2  27037  basellem2  27045  basellem5  27048  basellem9  27052  vma1  27129  sqff1o  27145  fsumfldivdiaglem  27152  chtub  27175  fsumvma2  27177  chpchtsum  27182  chpub  27183  logfaclbnd  27185  logfacbnd3  27186  logfacrlim  27187  logexprlim  27188  bcmono  27240  bposlem2  27248  bposlem5  27251  bposlem6  27252  lgsne0  27298  lgsquadlem1  27343  lgsquadlem2  27344  2sqblem  27394  2sqmod  27399  chebbnd1lem1  27432  chtppilimlem1  27436  chtppilimlem2  27437  chpchtlim  27442  rplogsumlem1  27447  dchrvmasumiflem1  27464  dchrisum0flblem2  27472  dchrisum0fno1  27474  dchrisum0lem2a  27480  dchrisum0lem3  27482  dirith  27492  mulog2sumlem1  27497  mulog2sumlem2  27498  log2sumbnd  27507  selberglem2  27509  logdivbnd  27519  selberg3lem1  27520  selberg4lem1  27523  pntrsumbnd2  27530  pntrlog2bndlem1  27540  pntrlog2bndlem5  27544  pntrlog2bndlem6  27546  pntpbnd1a  27548  pntpbnd1  27549  pntpbnd2  27550  pntibndlem3  27555  pntlemb  27560  pntlemn  27563  pntlemr  27565  pntlemj  27566  pntlemf  27568  pntlemo  27570  ostth2lem3  27598  ostth3  27601  addsuniflem  27993  ltsp1d  28007  negsid  28033  negsunif  28047  negleft  28050  mulsuniflem  28141  precsexlem9  28207  n0sge0  28330  zcuts  28399  halfcut  28450  addhalfcut  28451  pw2cut2  28454  bdayfinbndlem1  28459  footeq  28792  hlperpnel  28793  perpdragALT  28795  perpdrag  28796  colperp  28797  mideulem2  28802  opphllem  28803  opphllem3  28817  lmieu  28852  trgcopy  28872  sacgr  28899  acopyeu  28902  usgredgleordALT  29303  eucrctshift  30313  nvabs  30743  smcnlem  30768  ubthlem2  30942  minvecolem4  30951  htthlem  30988  normpyc  31217  nmophmi  32102  hstle  32301  hstles  32302  stlei  32311  f1rnen  32701  nnmulge  32812  fsumiunle  32902  sgnmulsgn  32915  wrdt2ind  33013  xrge0npcan  33080  gsumwrd2dccat  33139  trsp2cyc  33184  archirngz  33250  archiabllem1a  33252  archiabllem2a  33255  archiabllem2c  33256  elrgspnlem1  33303  elrgspn  33307  elrgspnsubrunlem2  33309  rprmasso  33585  q1pdir  33663  r1pquslmic  33671  evlextv  33686  mplvrpmga  33689  mplvrpmrhm  33691  drngdimgt0  33762  lbsdiflsp0  33770  fldextrspundgle  33822  fldext2rspun  33826  minplyirredlem  33854  madjusmdetlem2  33972  esumpinfval  34217  esumpinfsum  34221  esumpcvgval  34222  esum2d  34237  esumiun  34238  dya2icoseg  34421  omssubadd  34444  carsgsigalem  34459  carsggect  34462  carsgclctunlem3  34464  omsmeas  34467  eulerpartlems  34504  signsplypnf  34694  signsply0  34695  reprlt  34763  reprinfz1  34766  hgt750lemc  34791  hgt750lemf  34797  pthhashvtx  35310  resconn  35428  sinccvglem  35854  circum  35856  btwnxfr  36238  nn0prpwlem  36504  dnibndlem2  36739  unblimceq0  36767  irrdiff  37640  poimirlem7  37948  mblfinlem3  37980  mblfinlem4  37981  itg2addnclem3  37994  ftc1anc  38022  isbnd3  38105  cntotbnd  38117  bfp  38145  rrndstprj2  38152  1cvrjat  39921  3atlem1  39929  3atlem6  39934  llnmlplnN  39985  2llnjaN  40012  2lplnja  40065  dalem57  40175  dalawlem11  40327  dalawlem12  40328  lhp2lt  40447  lhpj1  40468  lhpm0atN  40475  4atexlemex2  40517  lautm  40540  cdleme17b  40733  cdleme20j  40764  cdleme30a  40824  cdlemg4c  41058  cdlemg17a  41107  cdlemg31c  41145  trljco  41186  cdlemk46  41394  dia2dimlem2  41511  cdlemm10N  41564  cdlemn10  41652  dihmeetlem1N  41736  dihglblem5apreN  41737  dihmeetlem15N  41767  mapdat  42113  lcmineqlem19  42486  lcmineqlem20  42487  aks4d1p1p5  42514  aks4d1p8d2  42524  aks4d1p8  42526  aks4d1p9  42527  hashscontpow  42561  dvdsexpnn  42765  mullt0b1d  42928  selvvvval  43018  evlselv  43020  mhphflem  43029  fltnlta  43096  3cubeslem1  43116  irrapxlem1  43250  irrapxlem4  43253  pell1qrgaplem  43301  pellfundglb  43313  rmspecfund  43337  monotoddzzfi  43370  rmynn  43384  jm2.24nn  43387  jm2.17c  43390  jm2.24  43391  acongeq  43411  jm2.20nn  43425  jm2.26lem3  43429  jm2.27a  43433  jm2.27c  43435  rmydioph  43442  jm3.1lem2  43446  frlmpwfi  43526  areaquad  43644  cantnf2  43753  rp-isfinite6  43945  frege129d  44190  leeq1d  44584  imo72b2lem0  44592  imo72b2  44599  cvgdvgrat  44740  radcnvrat  44741  hashnzfzclim  44749  isosctrlem1ALT  45360  cncmpmax  45463  iooabslt  45929  fmul01lt1lem2  46015  clim1fr1  46031  limcrecl  46059  climxrrelem  46177  liminflbuz2  46243  dvnprodlem1  46374  stoweidlem1  46429  stoweidlem11  46439  stoweidlem14  46442  stoweidlem24  46452  stoweidlem26  46454  wallispilem4  46496  wallispilem5  46497  stirlinglem1  46502  fourierdlem51  46585  fourierdlem65  46599  fouriersw  46659  2leaddle2  47746  2timesltsqm1  47827  sqrtpwpw2p  48001  lighneallem4a  48071  flnn0div2ge  49009  logbpw2m1  49043  functermclem  49982  amgmwlem  50277