Theorem eqbrtrrd 5139

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

Syntax hints:   → wi 4   = wceq 1567   class class class wbr 5113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114

This theorem is referenced by:  dftpos4  8240  dif1en  9145  fodomfi  9271  fmptssfisupp  9353  cnfcom2lem  9669  dmttrcl  9689  ttrclselem2  9694  ficardadju  10182  enfin1ai  10367  pwcfsdom  10567  fpwwe2lem6  10620  fpwwe2  10627  canthp1lem1  10636  1nqenq  10946  prlem936  11031  lemulge11  12076  supaddc  12181  supmul1  12183  mul2lt0llt0  13121  mul2lt0lgt0  13122  xaddge0  13283  xadddi2  13322  ltexp2a  14201  leexp2a  14207  nnlesq  14240  digit1  14272  faclbnd4lem1  14328  faclbnd6  14334  facavg  14336  prsshashgt1  14446  nehash2  14510  sgnmulsgn  15145  abs3dif  15382  abs2dif  15383  limsupgre  15531  rlimclim1  15595  rlimuni  15600  rlimres2  15611  rlimcn1  15638  rlimcn1b  15639  recn2  15651  imcn2  15652  rlimo1  15667  o1rlimmul  15669  iserex  15707  isercoll  15718  caucvgrlem2  15725  caucvgr  15726  iseraltlem3  15734  summolem2a  15765  fsumge1  15848  o1fsum  15864  isumrpcl  15896  climcnds  15904  harmonic  15912  mertenslem1  15937  prodmolem2a  15987  ege2le3  16143  efgt1p2  16169  efgt1p  16170  eirrlem  16259  rpnnen2lem11  16279  fsumdvds  16365  bitsfzo  16492  bitsmod  16493  bitscmp  16495  mulgcd  16605  dvdssqlem  16623  nn0seqcvgd  16627  mulgcddvds  16712  rpdvds  16717  qden1elz  16815  phimullem  16837  hashgcdlem  16846  hashgcdeq  16848  pcdvdstr  16935  pockthg  16965  prmreclem1  16975  4sqlem11  17014  ramub1lem1  17085  ramub1lem2  17086  mreexexlem4d  17702  sscid  17880  latmlej21  18535  latmlej22  18536  lubel  18569  efginvrel1  19797  odadd2  19918  odadd  19919  gexexlem  19921  cyggex2  19966  ablfacrplem  20136  ablfac1c  20142  ablfac1eu  20144  pgpfac1lem3a  20147  isabvd  20892  ornglmulle  20947  orngrmulle  20948  mptscmfsuppd  21026  znrrg  21683  frlmphl  21899  frlmup1  21916  f1linds  21943  selvvvval  22261  psdmplcl  22293  chcoeffeqlem  23010  lmcn2  23774  metrtri  24482  imasdsf1olem  24498  stdbdxmet  24640  nrmmetd  24699  nmmtri  24747  nlmvscnlem2  24810  blcvx  24923  recld2  24940  zdis  24942  opnreen  24957  cnheibor  25082  lebnumlem3  25090  nmoleub2lem3  25242  nmoleub2lem2  25243  nmoleub3  25246  ipcnlem2  25371  cmetcaulem  25415  nglmle  25429  cncmet  25449  csbren  25526  trirn  25527  minveclem4  25559  ovoliunlem1  25629  ovoliun2  25633  ovolscalem1  25640  ovolicopnf  25651  voliunlem2  25678  volsup  25683  ioorcl2  25699  uniiccvol  25707  uniioombllem4  25713  i1fd  25808  mbfi1fseqlem4  25845  itg2const2  25868  itg2eqa  25872  itg2split  25876  itg2i1fseqle  25881  itg2cnlem2  25889  dvcnv  26104  dveflem  26106  dvferm1lem  26111  dvlip2  26122  c1liplem1  26123  dvivthlem1  26135  lhop1lem  26140  dvcvx  26147  dvfsumle  26148  dvfsumabs  26150  dvfsumlem4  26156  dvfsumrlim2  26159  ftc1a  26164  tdeglem4  26185  deg1pwle  26245  fta1blem  26296  aalioulem3  26463  aaliou2b  26470  ulmbdd  26526  ulmdvlem1  26528  itgulm  26536  pserdvlem2  26556  abelthlem3  26561  abelthlem5  26563  abelthlem6  26564  abelthlem7  26566  tanregt0  26669  argimlt0  26743  logdivlti  26750  logcnlem3  26774  logcnlem4  26775  logtayl  26790  logtayl2  26792  cxple2  26827  cxpcn3lem  26877  cxpaddle  26882  rtprmirr  26890  isosctrlem1  26948  atantayl  27067  efrlim  27099  dfef2  27100  o1cxp  27104  cxp2lim  27106  divsqrtsumo1  27113  amgmlem  27119  logdifbnd  27123  emcllem7  27131  harmonicbnd4  27140  fsumharmonic  27141  lgamgulmlem2  27159  lgamgulmlem3  27160  lgamucov  27167  lgamcvg2  27184  gamcvg2  27189  ftalem2  27203  basellem2  27211  basellem5  27214  basellem9  27218  vma1  27295  sqff1o  27311  fsumfldivdiaglem  27318  chtub  27341  fsumvma2  27343  chpchtsum  27348  chpub  27349  logfaclbnd  27351  logfacbnd3  27352  logfacrlim  27353  logexprlim  27354  bcmono  27406  bposlem2  27414  bposlem5  27417  bposlem6  27418  lgsne0  27464  lgsquadlem1  27509  lgsquadlem2  27510  2sqblem  27560  2sqmod  27565  chebbnd1lem1  27598  chtppilimlem1  27602  chtppilimlem2  27603  chpchtlim  27608  rplogsumlem1  27613  dchrvmasumiflem1  27630  dchrisum0flblem2  27638  dchrisum0fno1  27640  dchrisum0lem2a  27646  dchrisum0lem3  27648  dirith  27658  mulog2sumlem1  27663  mulog2sumlem2  27664  log2sumbnd  27673  selberglem2  27675  logdivbnd  27685  selberg3lem1  27686  selberg4lem1  27689  pntrsumbnd2  27696  pntrlog2bndlem1  27706  pntrlog2bndlem5  27710  pntrlog2bndlem6  27712  pntpbnd1a  27714  pntpbnd1  27715  pntpbnd2  27716  pntibndlem3  27721  pntlemb  27726  pntlemn  27729  pntlemr  27731  pntlemj  27732  pntlemf  27734  pntlemo  27736  ostth2lem3  27764  ostth3  27767  addsuniflem  28159  ltsp1d  28173  negsid  28199  negsunif  28213  negleft  28216  mulsuniflem  28307  precsexlem9  28373  n0sge0  28496  zcuts  28565  halfcut  28616  addhalfcut  28617  pw2cut2  28620  bdayfinbndlem1  28625  footeq  28962  hlperpnel  28964  perpdragALT  28966  perpdrag  28967  colperp  28968  mideulem2  28973  opphllem  28974  opphllem3  28988  lmieu  29050  trgcopy  29071  sacgr  29098  acopyeu  29101  perpeqlem  29104  perpprlng  29152  usgredgleordALT  29524  eucrctshift  30534  nvabs  30964  smcnlem  30989  ubthlem2  31163  minvecolem4  31172  htthlem  31209  normpyc  31438  nmophmi  32323  hstle  32522  hstles  32523  stlei  32532  f1rnen  32913  nnmulge  33024  fsumiunle  33113  wrdt2ind  33213  xrge0npcan  33280  gsumwrd2dccat  33338  trsp2cyc  33383  archirngz  33449  archiabllem1a  33451  archiabllem2a  33454  archiabllem2c  33455  elrgspnlem1  33502  elrgspn  33506  elrgspnsubrunlem2  33508  rprmasso  33759  q1pdir  33837  r1pquslmic  33844  selvply1rhmlema  33852  selvply1rhmlem1  33854  evlextv  33876  mplvrpmga  33879  mplvrpmrhm  33881  drngdimgt0  33952  lbsdiflsp0  33960  fldextrspundgle  34012  fldext2rspun  34016  minplyirredlem  34044  madjusmdetlem2  34162  esumpinfval  34407  esumpinfsum  34411  esumpcvgval  34412  esum2d  34427  esumiun  34428  dya2icoseg  34611  omssubadd  34634  carsgsigalem  34649  carsggect  34652  carsgclctunlem3  34654  omsmeas  34657  eulerpartlems  34694  signsplypnf  34881  signsply0  34882  reprlt  34950  reprinfz1  34953  hgt750lemc  34978  hgt750lemf  34984  pthhashvtx  35518  resconn  35636  sinccvglem  36062  circum  36064  btwnxfr  36446  nn0prpwlem  36721  dnibndlem2  36956  unblimceq0  36984  irrdiff  37857  poimirlem7  38165  mblfinlem3  38197  mblfinlem4  38198  itg2addnclem3  38211  ftc1anc  38239  isbnd3  38322  cntotbnd  38334  bfp  38362  rrndstprj2  38369  1cvrjat  40138  3atlem1  40146  3atlem6  40151  llnmlplnN  40202  2llnjaN  40229  2lplnja  40282  dalem57  40392  dalawlem11  40544  dalawlem12  40545  lhp2lt  40664  lhpj1  40685  lhpm0atN  40692  4atexlemex2  40734  lautm  40757  cdleme17b  40950  cdleme20j  40981  cdleme30a  41041  cdlemg4c  41275  cdlemg17a  41324  cdlemg31c  41362  trljco  41403  cdlemk46  41611  dia2dimlem2  41728  cdlemm10N  41781  cdlemn10  41869  dihmeetlem1N  41953  dihglblem5apreN  41954  dihmeetlem15N  41984  mapdat  42330  lcmineqlem19  42703  lcmineqlem20  42704  aks4d1p1p5  42731  aks4d1p8d2  42741  aks4d1p8  42743  aks4d1p9  42744  hashscontpow  42778  dvdsexpnn  42983  mullt0b1d  43146  evlselv  43212  mhphflem  43219  fltnlta  43286  3cubeslem1  43306  irrapxlem1  43440  irrapxlem4  43443  pell1qrgaplem  43491  pellfundglb  43503  rmspecfund  43527  monotoddzzfi  43560  rmynn  43574  jm2.24nn  43577  jm2.17c  43580  jm2.24  43581  acongeq  43601  jm2.20nn  43615  jm2.26lem3  43619  jm2.27a  43623  jm2.27c  43625  rmydioph  43632  jm3.1lem2  43636  frlmpwfi  43716  areaquad  43834  cantnf2  43943  rp-isfinite6  44135  frege129d  44380  leeq1d  44774  imo72b2lem0  44782  imo72b2  44789  cvgdvgrat  44914  radcnvrat  44915  hashnzfzclim  44923  isosctrlem1ALT  45533  cncmpmax  45643  iooabslt  46106  fmul01lt1lem2  46192  clim1fr1  46208  limcrecl  46236  climxrrelem  46354  liminflbuz2  46420  dvnprodlem1  46551  stoweidlem1  46606  stoweidlem11  46616  stoweidlem14  46619  stoweidlem24  46629  stoweidlem26  46631  wallispilem4  46673  wallispilem5  46674  stirlinglem1  46679  fourierdlem51  46762  fourierdlem65  46776  fouriersw  46836  2leaddle2  47923  2timesltsqm1  48004  sqrtpwpw2p  48178  lighneallem4a  48248  flnn0div2ge  49197  logbpw2m1  49231  functermclem  50169  amgmwlem  50475