Theorem eqbrtrrd 5124

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

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

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101

This theorem is referenced by:  dftpos4  8197  dif1en  9098  fodomfi  9224  fodomfiOLD  9242  fmptssfisupp  9309  resfifsupp  9312  cnfcom2lem  9622  dmttrcl  9642  ttrclselem2  9647  ficardadju  10122  enfin1ai  10306  pwcfsdom  10506  fpwwe2lem6  10559  fpwwe2  10566  canthp1lem1  10575  1nqenq  10885  prlem936  10970  lemulge11  12016  supaddc  12121  supmul1  12123  mul2lt0llt0  13023  mul2lt0lgt0  13024  xaddge0  13185  xadddi2  13224  ltexp2a  14101  leexp2a  14107  nnlesq  14140  digit1  14172  faclbnd4lem1  14228  faclbnd6  14234  facavg  14236  prsshashgt1  14345  nehash2  14409  abs3dif  15267  abs2dif  15268  limsupgre  15416  rlimclim1  15480  rlimuni  15485  rlimres2  15496  rlimcn1  15523  rlimcn1b  15524  recn2  15536  imcn2  15537  rlimo1  15552  o1rlimmul  15554  iserex  15592  isercoll  15603  caucvgrlem2  15610  caucvgr  15611  iseraltlem3  15619  summolem2a  15650  fsumge1  15732  o1fsum  15748  isumrpcl  15778  climcnds  15786  harmonic  15794  mertenslem1  15819  prodmolem2a  15869  ege2le3  16025  efgt1p2  16051  efgt1p  16052  eirrlem  16141  rpnnen2lem11  16161  fsumdvds  16247  bitsfzo  16374  bitsmod  16375  bitscmp  16377  mulgcd  16487  dvdssqlem  16505  nn0seqcvgd  16509  mulgcddvds  16594  rpdvds  16599  qden1elz  16696  phimullem  16718  hashgcdlem  16727  hashgcdeq  16729  pcdvdstr  16816  pockthg  16846  prmreclem1  16856  4sqlem11  16895  ramub1lem1  16966  ramub1lem2  16967  mreexexlem4d  17582  sscid  17760  latmlej21  18415  latmlej22  18416  lubel  18449  efginvrel1  19669  odadd2  19790  odadd  19791  gexexlem  19793  cyggex2  19838  ablfacrplem  20008  ablfac1c  20014  ablfac1eu  20016  pgpfac1lem3a  20019  isabvd  20757  ornglmulle  20812  orngrmulle  20813  mptscmfsuppd  20891  znrrg  21532  frlmphl  21748  frlmup1  21765  f1linds  21792  psdmplcl  22117  chcoeffeqlem  22841  lmcn2  23605  metrtri  24313  imasdsf1olem  24329  stdbdxmet  24471  nrmmetd  24530  nmmtri  24578  nlmvscnlem2  24641  blcvx  24754  recld2  24771  zdis  24773  opnreen  24788  cnheibor  24922  lebnumlem3  24930  nmoleub2lem3  25083  nmoleub2lem2  25084  nmoleub3  25087  ipcnlem2  25212  cmetcaulem  25256  nglmle  25270  cncmet  25290  csbren  25367  trirn  25368  minveclem4  25400  ovoliunlem1  25471  ovoliun2  25475  ovolscalem1  25482  ovolicopnf  25493  voliunlem2  25520  volsup  25525  ioorcl2  25541  uniiccvol  25549  uniioombllem4  25555  i1fd  25650  mbfi1fseqlem4  25687  itg2const2  25710  itg2eqa  25714  itg2split  25718  itg2i1fseqle  25723  itg2cnlem2  25731  dvcnv  25949  dveflem  25951  dvferm1lem  25956  dvlip2  25968  c1liplem1  25969  dvivthlem1  25981  lhop1lem  25986  dvcvx  25993  dvfsumle  25994  dvfsumleOLD  25995  dvfsumabs  25997  dvfsumlem4  26004  dvfsumrlim2  26007  ftc1a  26012  tdeglem4  26033  deg1pwle  26093  fta1blem  26144  aalioulem3  26310  aaliou2b  26317  ulmbdd  26375  ulmdvlem1  26377  itgulm  26385  pserdvlem2  26406  abelthlem3  26411  abelthlem5  26413  abelthlem6  26414  abelthlem7  26416  tanregt0  26516  argimlt0  26590  logdivlti  26597  logcnlem3  26621  logcnlem4  26622  logtayl  26637  logtayl2  26639  cxple2  26674  cxpcn3lem  26725  cxpaddle  26730  rtprmirr  26738  isosctrlem1  26796  atantayl  26915  efrlim  26947  efrlimOLD  26948  dfef2  26949  o1cxp  26953  cxp2lim  26955  divsqrtsumo1  26962  amgmlem  26968  logdifbnd  26972  emcllem7  26980  harmonicbnd4  26989  fsumharmonic  26990  lgamgulmlem2  27008  lgamgulmlem3  27009  lgamucov  27016  lgamcvg2  27033  gamcvg2  27038  ftalem2  27052  basellem2  27060  basellem5  27063  basellem9  27067  vma1  27144  sqff1o  27160  fsumfldivdiaglem  27167  chtub  27191  fsumvma2  27193  chpchtsum  27198  chpub  27199  logfaclbnd  27201  logfacbnd3  27202  logfacrlim  27203  logexprlim  27204  bcmono  27256  bposlem2  27264  bposlem5  27267  bposlem6  27268  lgsne0  27314  lgsquadlem1  27359  lgsquadlem2  27360  2sqblem  27410  2sqmod  27415  chebbnd1lem1  27448  chtppilimlem1  27452  chtppilimlem2  27453  chpchtlim  27458  rplogsumlem1  27463  dchrvmasumiflem1  27480  dchrisum0flblem2  27488  dchrisum0fno1  27490  dchrisum0lem2a  27496  dchrisum0lem3  27498  dirith  27508  mulog2sumlem1  27513  mulog2sumlem2  27514  log2sumbnd  27523  selberglem2  27525  logdivbnd  27535  selberg3lem1  27536  selberg4lem1  27539  pntrsumbnd2  27546  pntrlog2bndlem1  27556  pntrlog2bndlem5  27560  pntrlog2bndlem6  27562  pntpbnd1a  27564  pntpbnd1  27565  pntpbnd2  27566  pntibndlem3  27571  pntlemb  27576  pntlemn  27579  pntlemr  27581  pntlemj  27582  pntlemf  27584  pntlemo  27586  ostth2lem3  27614  ostth3  27617  addsuniflem  28009  ltsp1d  28023  negsid  28049  negsunif  28063  negleft  28066  mulsuniflem  28157  precsexlem9  28223  n0sge0  28346  zcuts  28415  halfcut  28466  addhalfcut  28467  pw2cut2  28470  bdayfinbndlem1  28475  footeq  28808  hlperpnel  28809  perpdragALT  28811  perpdrag  28812  colperp  28813  mideulem2  28818  opphllem  28819  opphllem3  28833  lmieu  28868  trgcopy  28888  sacgr  28915  acopyeu  28918  usgredgleordALT  29319  eucrctshift  30330  nvabs  30760  smcnlem  30785  ubthlem2  30959  minvecolem4  30968  htthlem  31005  normpyc  31234  nmophmi  32119  hstle  32318  hstles  32319  stlei  32328  f1rnen  32718  nnmulge  32829  fsumiunle  32921  sgnmulsgn  32934  wrdt2ind  33046  xrge0npcan  33113  gsumwrd2dccat  33172  trsp2cyc  33217  archirngz  33283  archiabllem1a  33285  archiabllem2a  33288  archiabllem2c  33289  elrgspnlem1  33336  elrgspn  33340  elrgspnsubrunlem2  33342  rprmasso  33618  q1pdir  33696  r1pquslmic  33704  evlextv  33719  mplvrpmga  33722  mplvrpmrhm  33724  drngdimgt0  33796  lbsdiflsp0  33804  fldextrspundgle  33856  fldext2rspun  33860  minplyirredlem  33888  madjusmdetlem2  34006  esumpinfval  34251  esumpinfsum  34255  esumpcvgval  34256  esum2d  34271  esumiun  34272  dya2icoseg  34455  omssubadd  34478  carsgsigalem  34493  carsggect  34496  carsgclctunlem3  34498  omsmeas  34501  eulerpartlems  34538  signsplypnf  34728  signsply0  34729  reprlt  34797  reprinfz1  34800  hgt750lemc  34825  hgt750lemf  34831  pthhashvtx  35344  resconn  35462  sinccvglem  35888  circum  35890  btwnxfr  36272  nn0prpwlem  36538  dnibndlem2  36701  unblimceq0  36729  irrdiff  37581  poimirlem7  37878  mblfinlem3  37910  mblfinlem4  37911  itg2addnclem3  37924  ftc1anc  37952  isbnd3  38035  cntotbnd  38047  bfp  38075  rrndstprj2  38082  1cvrjat  39851  3atlem1  39859  3atlem6  39864  llnmlplnN  39915  2llnjaN  39942  2lplnja  39995  dalem57  40105  dalawlem11  40257  dalawlem12  40258  lhp2lt  40377  lhpj1  40398  lhpm0atN  40405  4atexlemex2  40447  lautm  40470  cdleme17b  40663  cdleme20j  40694  cdleme30a  40754  cdlemg4c  40988  cdlemg17a  41037  cdlemg31c  41075  trljco  41116  cdlemk46  41324  dia2dimlem2  41441  cdlemm10N  41494  cdlemn10  41582  dihmeetlem1N  41666  dihglblem5apreN  41667  dihmeetlem15N  41697  mapdat  42043  lcmineqlem19  42417  lcmineqlem20  42418  aks4d1p1p5  42445  aks4d1p8d2  42455  aks4d1p8  42457  aks4d1p9  42458  hashscontpow  42492  dvdsexpnn  42703  mullt0b1d  42853  selvvvval  42943  evlselv  42945  mhphflem  42954  fltnlta  43021  3cubeslem1  43041  irrapxlem1  43179  irrapxlem4  43182  pell1qrgaplem  43230  pellfundglb  43242  rmspecfund  43266  monotoddzzfi  43299  rmynn  43313  jm2.24nn  43316  jm2.17c  43319  jm2.24  43320  acongeq  43340  jm2.20nn  43354  jm2.26lem3  43358  jm2.27a  43362  jm2.27c  43364  rmydioph  43371  jm3.1lem2  43375  frlmpwfi  43455  areaquad  43573  cantnf2  43682  rp-isfinite6  43874  frege129d  44119  leeq1d  44513  imo72b2lem0  44521  imo72b2  44528  cvgdvgrat  44669  radcnvrat  44670  hashnzfzclim  44678  isosctrlem1ALT  45289  cncmpmax  45392  iooabslt  45859  fmul01lt1lem2  45945  clim1fr1  45961  limcrecl  45989  climxrrelem  46107  liminflbuz2  46173  dvnprodlem1  46304  stoweidlem1  46359  stoweidlem11  46369  stoweidlem14  46372  stoweidlem24  46382  stoweidlem26  46384  wallispilem4  46426  wallispilem5  46427  stirlinglem1  46432  fourierdlem51  46515  fourierdlem65  46529  fouriersw  46589  2leaddle2  47658  sqrtpwpw2p  47898  lighneallem4a  47968  flnn0div2ge  48893  logbpw2m1  48927  functermclem  49866  amgmwlem  50161