Theorem eqbrtrrd 5148

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 5146	1 ⊢ (𝜑 → 𝐵𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5124

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125

This theorem is referenced by:  dftpos4  8249  dif1en  9179  dif1enOLD  9181  fodomfi  9327  fodomfiOLD  9347  fmptssfisupp  9411  resfifsupp  9414  cnfcom2lem  9720  dmttrcl  9740  ttrclselem2  9745  ficardadju  10219  enfin1ai  10403  pwcfsdom  10602  fpwwe2lem6  10655  fpwwe2  10662  canthp1lem1  10671  1nqenq  10981  prlem936  11066  lemulge11  12109  supaddc  12214  supmul1  12216  mul2lt0llt0  13118  mul2lt0lgt0  13119  xaddge0  13279  xadddi2  13318  ltexp2a  14189  leexp2a  14195  nnlesq  14228  digit1  14260  faclbnd4lem1  14316  faclbnd6  14322  facavg  14324  prsshashgt1  14433  nehash2  14497  abs3dif  15355  abs2dif  15356  limsupgre  15502  rlimclim1  15566  rlimuni  15571  rlimres2  15582  rlimcn1  15609  rlimcn1b  15610  recn2  15622  imcn2  15623  rlimo1  15638  o1rlimmul  15640  iserex  15678  isercoll  15689  caucvgrlem2  15696  caucvgr  15697  iseraltlem3  15705  summolem2a  15736  fsumge1  15818  o1fsum  15834  isumrpcl  15864  climcnds  15872  harmonic  15880  mertenslem1  15905  prodmolem2a  15955  ege2le3  16111  efgt1p2  16137  efgt1p  16138  eirrlem  16227  rpnnen2lem11  16247  fsumdvds  16332  bitsfzo  16459  bitsmod  16460  bitscmp  16462  mulgcd  16572  dvdssqlem  16590  nn0seqcvgd  16594  mulgcddvds  16679  rpdvds  16684  qden1elz  16781  phimullem  16803  hashgcdlem  16812  hashgcdeq  16814  pcdvdstr  16901  pockthg  16931  prmreclem1  16941  4sqlem11  16980  ramub1lem1  17051  ramub1lem2  17052  mreexexlem4d  17664  sscid  17842  latmlej21  18495  latmlej22  18496  lubel  18529  efginvrel1  19714  odadd2  19835  odadd  19836  gexexlem  19838  cyggex2  19883  ablfacrplem  20053  ablfac1c  20059  ablfac1eu  20061  pgpfac1lem3a  20064  isabvd  20777  mptscmfsuppd  20890  znrrg  21531  frlmphl  21746  frlmup1  21763  f1linds  21790  psdmplcl  22105  chcoeffeqlem  22828  lmcn2  23592  metrtri  24301  imasdsf1olem  24317  stdbdxmet  24459  nrmmetd  24518  nmmtri  24566  nlmvscnlem2  24629  blcvx  24742  recld2  24759  zdis  24761  opnreen  24776  cnheibor  24910  lebnumlem3  24918  nmoleub2lem3  25071  nmoleub2lem2  25072  nmoleub3  25075  ipcnlem2  25201  cmetcaulem  25245  nglmle  25259  cncmet  25279  csbren  25356  trirn  25357  minveclem4  25389  ovoliunlem1  25460  ovoliun2  25464  ovolscalem1  25471  ovolicopnf  25482  voliunlem2  25509  volsup  25514  ioorcl2  25530  uniiccvol  25538  uniioombllem4  25544  i1fd  25639  mbfi1fseqlem4  25676  itg2const2  25699  itg2eqa  25703  itg2split  25707  itg2i1fseqle  25712  itg2cnlem2  25720  dvcnv  25938  dveflem  25940  dvferm1lem  25945  dvlip2  25957  c1liplem1  25958  dvivthlem1  25970  lhop1lem  25975  dvcvx  25982  dvfsumle  25983  dvfsumleOLD  25984  dvfsumabs  25986  dvfsumlem4  25993  dvfsumrlim2  25996  ftc1a  26001  tdeglem4  26022  deg1pwle  26082  fta1blem  26133  aalioulem3  26299  aaliou2b  26306  ulmbdd  26364  ulmdvlem1  26366  itgulm  26374  pserdvlem2  26395  abelthlem3  26400  abelthlem5  26402  abelthlem6  26403  abelthlem7  26405  tanregt0  26505  argimlt0  26579  logdivlti  26586  logcnlem3  26610  logcnlem4  26611  logtayl  26626  logtayl2  26628  cxple2  26663  cxpcn3lem  26714  cxpaddle  26719  rtprmirr  26727  isosctrlem1  26785  atantayl  26904  efrlim  26936  efrlimOLD  26937  dfef2  26938  o1cxp  26942  cxp2lim  26944  divsqrtsumo1  26951  amgmlem  26957  logdifbnd  26961  emcllem7  26969  harmonicbnd4  26978  fsumharmonic  26979  lgamgulmlem2  26997  lgamgulmlem3  26998  lgamucov  27005  lgamcvg2  27022  gamcvg2  27027  ftalem2  27041  basellem2  27049  basellem5  27052  basellem9  27056  vma1  27133  sqff1o  27149  fsumfldivdiaglem  27156  chtub  27180  fsumvma2  27182  chpchtsum  27187  chpub  27188  logfaclbnd  27190  logfacbnd3  27191  logfacrlim  27192  logexprlim  27193  bcmono  27245  bposlem2  27253  bposlem5  27256  bposlem6  27257  lgsne0  27303  lgsquadlem1  27348  lgsquadlem2  27349  2sqblem  27399  2sqmod  27404  chebbnd1lem1  27437  chtppilimlem1  27441  chtppilimlem2  27442  chpchtlim  27447  rplogsumlem1  27452  dchrvmasumiflem1  27469  dchrisum0flblem2  27477  dchrisum0fno1  27479  dchrisum0lem2a  27485  dchrisum0lem3  27487  dirith  27497  mulog2sumlem1  27502  mulog2sumlem2  27503  log2sumbnd  27512  selberglem2  27514  logdivbnd  27524  selberg3lem1  27525  selberg4lem1  27528  pntrsumbnd2  27535  pntrlog2bndlem1  27545  pntrlog2bndlem5  27549  pntrlog2bndlem6  27551  pntpbnd1a  27553  pntpbnd1  27554  pntpbnd2  27555  pntibndlem3  27560  pntlemb  27565  pntlemn  27568  pntlemr  27570  pntlemj  27571  pntlemf  27573  pntlemo  27575  ostth2lem3  27603  ostth3  27606  addsuniflem  27965  sltp1d  27979  negsid  28004  negsunif  28018  mulsuniflem  28109  precsexlem9  28174  n0sge0  28287  zscut  28352  halfcut  28390  addhalfcut  28391  footeq  28708  hlperpnel  28709  perpdragALT  28711  perpdrag  28712  colperp  28713  mideulem2  28718  opphllem  28719  opphllem3  28733  lmieu  28768  trgcopy  28788  sacgr  28815  acopyeu  28818  usgredgleordALT  29218  eucrctshift  30229  nvabs  30658  smcnlem  30683  ubthlem2  30857  minvecolem4  30866  htthlem  30903  normpyc  31132  nmophmi  32017  hstle  32216  hstles  32217  stlei  32226  f1rnen  32612  nnmulge  32721  fsumiunle  32813  sgnmulsgn  32826  wrdt2ind  32934  xrge0npcan  33020  gsumwrd2dccat  33066  trsp2cyc  33139  archirngz  33192  archiabllem1a  33194  archiabllem2a  33197  archiabllem2c  33198  elrgspnlem1  33242  elrgspn  33246  elrgspnsubrunlem2  33248  ornglmulle  33332  orngrmulle  33333  rprmasso  33545  q1pdir  33617  r1pquslmic  33625  drngdimgt0  33663  lbsdiflsp0  33671  fldextrspundgle  33724  fldext2rspun  33728  minplyirredlem  33749  madjusmdetlem2  33864  esumpinfval  34109  esumpinfsum  34113  esumpcvgval  34114  esum2d  34129  esumiun  34130  dya2icoseg  34314  omssubadd  34337  carsgsigalem  34352  carsggect  34355  carsgclctunlem3  34357  omsmeas  34360  eulerpartlems  34397  signsplypnf  34587  signsply0  34588  reprlt  34656  reprinfz1  34659  hgt750lemc  34684  hgt750lemf  34690  pthhashvtx  35155  resconn  35273  sinccvglem  35699  circum  35701  btwnxfr  36079  nn0prpwlem  36345  dnibndlem2  36502  unblimceq0  36530  irrdiff  37349  poimirlem7  37656  mblfinlem3  37688  mblfinlem4  37689  itg2addnclem3  37702  ftc1anc  37730  isbnd3  37813  cntotbnd  37825  bfp  37853  rrndstprj2  37860  1cvrjat  39499  3atlem1  39507  3atlem6  39512  llnmlplnN  39563  2llnjaN  39590  2lplnja  39643  dalem57  39753  dalawlem11  39905  dalawlem12  39906  lhp2lt  40025  lhpj1  40046  lhpm0atN  40053  4atexlemex2  40095  lautm  40118  cdleme17b  40311  cdleme20j  40342  cdleme30a  40402  cdlemg4c  40636  cdlemg17a  40685  cdlemg31c  40723  trljco  40764  cdlemk46  40972  dia2dimlem2  41089  cdlemm10N  41142  cdlemn10  41230  dihmeetlem1N  41314  dihglblem5apreN  41315  dihmeetlem15N  41345  mapdat  41691  lcmineqlem19  42065  lcmineqlem20  42066  aks4d1p1p5  42093  aks4d1p8d2  42103  aks4d1p8  42105  aks4d1p9  42106  hashscontpow  42140  dvdsexpnn  42351  selvvvval  42583  evlselv  42585  mhphflem  42594  fltnlta  42661  3cubeslem1  42682  irrapxlem1  42820  irrapxlem4  42823  pell1qrgaplem  42871  pellfundglb  42883  rmspecfund  42907  monotoddzzfi  42941  rmynn  42955  jm2.24nn  42958  jm2.17c  42961  jm2.24  42962  acongeq  42982  jm2.20nn  42996  jm2.26lem3  43000  jm2.27a  43004  jm2.27c  43006  rmydioph  43013  jm3.1lem2  43017  frlmpwfi  43097  areaquad  43215  cantnf2  43324  rp-isfinite6  43517  frege129d  43762  leeq1d  44156  imo72b2lem0  44164  imo72b2  44171  cvgdvgrat  44312  radcnvrat  44313  hashnzfzclim  44321  isosctrlem1ALT  44933  cncmpmax  45036  iooabslt  45508  fmul01lt1lem2  45594  clim1fr1  45610  limcrecl  45638  climxrrelem  45758  liminflbuz2  45824  dvnprodlem1  45955  stoweidlem1  46010  stoweidlem11  46020  stoweidlem14  46023  stoweidlem24  46033  stoweidlem26  46035  wallispilem4  46077  wallispilem5  46078  stirlinglem1  46083  fourierdlem51  46166  fourierdlem65  46180  fouriersw  46240  2leaddle2  47307  sqrtpwpw2p  47532  lighneallem4a  47602  flnn0div2ge  48493  logbpw2m1  48527  functermclem  49372  amgmwlem  49646