Theorem eqbrtrrd 5112

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

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3393  df-v 3435  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5089

This theorem is referenced by:  dftpos4  8169  dif1en  9065  fodomfi  9190  fodomfiOLD  9208  fmptssfisupp  9272  resfifsupp  9275  cnfcom2lem  9585  dmttrcl  9605  ttrclselem2  9610  ficardadju  10082  enfin1ai  10266  pwcfsdom  10465  fpwwe2lem6  10518  fpwwe2  10525  canthp1lem1  10534  1nqenq  10844  prlem936  10929  lemulge11  11975  supaddc  12080  supmul1  12082  mul2lt0llt0  12987  mul2lt0lgt0  12988  xaddge0  13148  xadddi2  13187  ltexp2a  14061  leexp2a  14067  nnlesq  14100  digit1  14132  faclbnd4lem1  14188  faclbnd6  14194  facavg  14196  prsshashgt1  14305  nehash2  14369  abs3dif  15226  abs2dif  15227  limsupgre  15375  rlimclim1  15439  rlimuni  15444  rlimres2  15455  rlimcn1  15482  rlimcn1b  15483  recn2  15495  imcn2  15496  rlimo1  15511  o1rlimmul  15513  iserex  15551  isercoll  15562  caucvgrlem2  15569  caucvgr  15570  iseraltlem3  15578  summolem2a  15609  fsumge1  15691  o1fsum  15707  isumrpcl  15737  climcnds  15745  harmonic  15753  mertenslem1  15778  prodmolem2a  15828  ege2le3  15984  efgt1p2  16010  efgt1p  16011  eirrlem  16100  rpnnen2lem11  16120  fsumdvds  16206  bitsfzo  16333  bitsmod  16334  bitscmp  16336  mulgcd  16446  dvdssqlem  16464  nn0seqcvgd  16468  mulgcddvds  16553  rpdvds  16558  qden1elz  16655  phimullem  16677  hashgcdlem  16686  hashgcdeq  16688  pcdvdstr  16775  pockthg  16805  prmreclem1  16815  4sqlem11  16854  ramub1lem1  16925  ramub1lem2  16926  mreexexlem4d  17540  sscid  17718  latmlej21  18373  latmlej22  18374  lubel  18407  efginvrel1  19594  odadd2  19715  odadd  19716  gexexlem  19718  cyggex2  19763  ablfacrplem  19933  ablfac1c  19939  ablfac1eu  19941  pgpfac1lem3a  19944  isabvd  20681  ornglmulle  20736  orngrmulle  20737  mptscmfsuppd  20815  znrrg  21456  frlmphl  21672  frlmup1  21689  f1linds  21716  psdmplcl  22031  chcoeffeqlem  22754  lmcn2  23518  metrtri  24226  imasdsf1olem  24242  stdbdxmet  24384  nrmmetd  24443  nmmtri  24491  nlmvscnlem2  24554  blcvx  24667  recld2  24684  zdis  24686  opnreen  24701  cnheibor  24835  lebnumlem3  24843  nmoleub2lem3  24996  nmoleub2lem2  24997  nmoleub3  25000  ipcnlem2  25125  cmetcaulem  25169  nglmle  25183  cncmet  25203  csbren  25280  trirn  25281  minveclem4  25313  ovoliunlem1  25384  ovoliun2  25388  ovolscalem1  25395  ovolicopnf  25406  voliunlem2  25433  volsup  25438  ioorcl2  25454  uniiccvol  25462  uniioombllem4  25468  i1fd  25563  mbfi1fseqlem4  25600  itg2const2  25623  itg2eqa  25627  itg2split  25631  itg2i1fseqle  25636  itg2cnlem2  25644  dvcnv  25862  dveflem  25864  dvferm1lem  25869  dvlip2  25881  c1liplem1  25882  dvivthlem1  25894  lhop1lem  25899  dvcvx  25906  dvfsumle  25907  dvfsumleOLD  25908  dvfsumabs  25910  dvfsumlem4  25917  dvfsumrlim2  25920  ftc1a  25925  tdeglem4  25946  deg1pwle  26006  fta1blem  26057  aalioulem3  26223  aaliou2b  26230  ulmbdd  26288  ulmdvlem1  26290  itgulm  26298  pserdvlem2  26319  abelthlem3  26324  abelthlem5  26326  abelthlem6  26327  abelthlem7  26329  tanregt0  26429  argimlt0  26503  logdivlti  26510  logcnlem3  26534  logcnlem4  26535  logtayl  26550  logtayl2  26552  cxple2  26587  cxpcn3lem  26638  cxpaddle  26643  rtprmirr  26651  isosctrlem1  26709  atantayl  26828  efrlim  26860  efrlimOLD  26861  dfef2  26862  o1cxp  26866  cxp2lim  26868  divsqrtsumo1  26875  amgmlem  26881  logdifbnd  26885  emcllem7  26893  harmonicbnd4  26902  fsumharmonic  26903  lgamgulmlem2  26921  lgamgulmlem3  26922  lgamucov  26929  lgamcvg2  26946  gamcvg2  26951  ftalem2  26965  basellem2  26973  basellem5  26976  basellem9  26980  vma1  27057  sqff1o  27073  fsumfldivdiaglem  27080  chtub  27104  fsumvma2  27106  chpchtsum  27111  chpub  27112  logfaclbnd  27114  logfacbnd3  27115  logfacrlim  27116  logexprlim  27117  bcmono  27169  bposlem2  27177  bposlem5  27180  bposlem6  27181  lgsne0  27227  lgsquadlem1  27272  lgsquadlem2  27273  2sqblem  27323  2sqmod  27328  chebbnd1lem1  27361  chtppilimlem1  27365  chtppilimlem2  27366  chpchtlim  27371  rplogsumlem1  27376  dchrvmasumiflem1  27393  dchrisum0flblem2  27401  dchrisum0fno1  27403  dchrisum0lem2a  27409  dchrisum0lem3  27411  dirith  27421  mulog2sumlem1  27426  mulog2sumlem2  27427  log2sumbnd  27436  selberglem2  27438  logdivbnd  27448  selberg3lem1  27449  selberg4lem1  27452  pntrsumbnd2  27459  pntrlog2bndlem1  27469  pntrlog2bndlem5  27473  pntrlog2bndlem6  27475  pntpbnd1a  27477  pntpbnd1  27478  pntpbnd2  27479  pntibndlem3  27484  pntlemb  27489  pntlemn  27492  pntlemr  27494  pntlemj  27495  pntlemf  27497  pntlemo  27499  ostth2lem3  27527  ostth3  27530  addsuniflem  27898  sltp1d  27912  negsid  27937  negsunif  27951  mulsuniflem  28042  precsexlem9  28107  n0sge0  28220  zscut  28285  halfcut  28332  addhalfcut  28333  pw2cut2  28336  footeq  28656  hlperpnel  28657  perpdragALT  28659  perpdrag  28660  colperp  28661  mideulem2  28666  opphllem  28667  opphllem3  28681  lmieu  28716  trgcopy  28736  sacgr  28763  acopyeu  28766  usgredgleordALT  29166  eucrctshift  30174  nvabs  30603  smcnlem  30628  ubthlem2  30802  minvecolem4  30811  htthlem  30848  normpyc  31077  nmophmi  31962  hstle  32161  hstles  32162  stlei  32171  f1rnen  32562  nnmulge  32674  fsumiunle  32767  sgnmulsgn  32780  wrdt2ind  32890  xrge0npcan  32969  gsumwrd2dccat  33015  trsp2cyc  33060  archirngz  33126  archiabllem1a  33128  archiabllem2a  33131  archiabllem2c  33132  elrgspnlem1  33177  elrgspn  33181  elrgspnsubrunlem2  33183  rprmasso  33458  q1pdir  33531  r1pquslmic  33539  mplvrpmga  33543  mplvrpmrhm  33545  drngdimgt0  33599  lbsdiflsp0  33607  fldextrspundgle  33659  fldext2rspun  33663  minplyirredlem  33691  madjusmdetlem2  33809  esumpinfval  34054  esumpinfsum  34058  esumpcvgval  34059  esum2d  34074  esumiun  34075  dya2icoseg  34258  omssubadd  34281  carsgsigalem  34296  carsggect  34299  carsgclctunlem3  34301  omsmeas  34304  eulerpartlems  34341  signsplypnf  34531  signsply0  34532  reprlt  34600  reprinfz1  34603  hgt750lemc  34628  hgt750lemf  34634  pthhashvtx  35118  resconn  35236  sinccvglem  35662  circum  35664  btwnxfr  36047  nn0prpwlem  36313  dnibndlem2  36470  unblimceq0  36498  irrdiff  37317  poimirlem7  37624  mblfinlem3  37656  mblfinlem4  37657  itg2addnclem3  37670  ftc1anc  37698  isbnd3  37781  cntotbnd  37793  bfp  37821  rrndstprj2  37828  1cvrjat  39471  3atlem1  39479  3atlem6  39484  llnmlplnN  39535  2llnjaN  39562  2lplnja  39615  dalem57  39725  dalawlem11  39877  dalawlem12  39878  lhp2lt  39997  lhpj1  40018  lhpm0atN  40025  4atexlemex2  40067  lautm  40090  cdleme17b  40283  cdleme20j  40314  cdleme30a  40374  cdlemg4c  40608  cdlemg17a  40657  cdlemg31c  40695  trljco  40736  cdlemk46  40944  dia2dimlem2  41061  cdlemm10N  41114  cdlemn10  41202  dihmeetlem1N  41286  dihglblem5apreN  41287  dihmeetlem15N  41317  mapdat  41663  lcmineqlem19  42037  lcmineqlem20  42038  aks4d1p1p5  42065  aks4d1p8d2  42075  aks4d1p8  42077  aks4d1p9  42078  hashscontpow  42112  dvdsexpnn  42323  mullt0b1d  42473  selvvvval  42575  evlselv  42577  mhphflem  42586  fltnlta  42653  3cubeslem1  42674  irrapxlem1  42812  irrapxlem4  42815  pell1qrgaplem  42863  pellfundglb  42875  rmspecfund  42899  monotoddzzfi  42932  rmynn  42946  jm2.24nn  42949  jm2.17c  42952  jm2.24  42953  acongeq  42973  jm2.20nn  42987  jm2.26lem3  42991  jm2.27a  42995  jm2.27c  42997  rmydioph  43004  jm3.1lem2  43008  frlmpwfi  43088  areaquad  43206  cantnf2  43315  rp-isfinite6  43508  frege129d  43753  leeq1d  44147  imo72b2lem0  44155  imo72b2  44162  cvgdvgrat  44303  radcnvrat  44304  hashnzfzclim  44312  isosctrlem1ALT  44923  cncmpmax  45026  iooabslt  45496  fmul01lt1lem2  45582  clim1fr1  45598  limcrecl  45626  climxrrelem  45744  liminflbuz2  45810  dvnprodlem1  45941  stoweidlem1  45996  stoweidlem11  46006  stoweidlem14  46009  stoweidlem24  46019  stoweidlem26  46021  wallispilem4  46063  wallispilem5  46064  stirlinglem1  46069  fourierdlem51  46152  fourierdlem65  46166  fouriersw  46226  2leaddle2  47296  sqrtpwpw2p  47536  lighneallem4a  47606  flnn0div2ge  48532  logbpw2m1  48566  functermclem  49506  amgmwlem  49801