Theorem eqbrtrrd 5149

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

Syntax hints:   → wi 4   = wceq 1539   class class class wbr 5125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3421  df-v 3466  df-dif 3936  df-un 3938  df-ss 3950  df-nul 4316  df-if 4508  df-sn 4609  df-pr 4611  df-op 4615  df-br 5126

This theorem is referenced by:  dftpos4  8253  dif1en  9183  dif1enOLD  9185  fodomfi  9333  fodomfiOLD  9353  fmptssfisupp  9417  resfifsupp  9420  cnfcom2lem  9724  dmttrcl  9744  ttrclselem2  9749  ficardadju  10223  enfin1ai  10407  pwcfsdom  10606  fpwwe2lem6  10659  fpwwe2  10666  canthp1lem1  10675  1nqenq  10985  prlem936  11070  lemulge11  12113  supaddc  12218  supmul1  12220  mul2lt0llt0  13122  mul2lt0lgt0  13123  xaddge0  13283  xadddi2  13322  ltexp2a  14189  leexp2a  14195  nnlesq  14227  digit1  14259  faclbnd4lem1  14315  faclbnd6  14321  facavg  14323  prsshashgt1  14432  nehash2  14496  abs3dif  15353  abs2dif  15354  limsupgre  15500  rlimclim1  15564  rlimuni  15569  rlimres2  15580  rlimcn1  15607  rlimcn1b  15608  recn2  15620  imcn2  15621  rlimo1  15636  o1rlimmul  15638  iserex  15676  isercoll  15687  caucvgrlem2  15694  caucvgr  15695  iseraltlem3  15703  summolem2a  15734  fsumge1  15816  o1fsum  15832  isumrpcl  15862  climcnds  15870  harmonic  15878  mertenslem1  15903  prodmolem2a  15953  ege2le3  16109  efgt1p2  16133  efgt1p  16134  eirrlem  16223  rpnnen2lem11  16243  fsumdvds  16328  bitsfzo  16455  bitsmod  16456  bitscmp  16458  mulgcd  16568  dvdssqlem  16586  nn0seqcvgd  16590  mulgcddvds  16675  rpdvds  16680  qden1elz  16777  phimullem  16799  hashgcdlem  16808  hashgcdeq  16810  pcdvdstr  16897  pockthg  16927  prmreclem1  16937  4sqlem11  16976  ramub1lem1  17047  ramub1lem2  17048  mreexexlem4d  17666  sscid  17844  latmlej21  18499  latmlej22  18500  lubel  18533  efginvrel1  19719  odadd2  19840  odadd  19841  gexexlem  19843  cyggex2  19888  ablfacrplem  20058  ablfac1c  20064  ablfac1eu  20066  pgpfac1lem3a  20069  isabvd  20786  mptscmfsuppd  20899  znrrg  21551  frlmphl  21768  frlmup1  21785  f1linds  21812  psdmplcl  22133  chcoeffeqlem  22858  lmcn2  23622  metrtri  24331  imasdsf1olem  24347  stdbdxmet  24491  nrmmetd  24550  nmmtri  24598  nlmvscnlem2  24661  blcvx  24774  recld2  24791  zdis  24793  opnreen  24808  cnheibor  24942  lebnumlem3  24950  nmoleub2lem3  25103  nmoleub2lem2  25104  nmoleub3  25107  ipcnlem2  25233  cmetcaulem  25277  nglmle  25291  cncmet  25311  csbren  25388  trirn  25389  minveclem4  25421  ovoliunlem1  25492  ovoliun2  25496  ovolscalem1  25503  ovolicopnf  25514  voliunlem2  25541  volsup  25546  ioorcl2  25562  uniiccvol  25570  uniioombllem4  25576  i1fd  25671  mbfi1fseqlem4  25708  itg2const2  25731  itg2eqa  25735  itg2split  25739  itg2i1fseqle  25744  itg2cnlem2  25752  dvcnv  25970  dveflem  25972  dvferm1lem  25977  dvlip2  25989  c1liplem1  25990  dvivthlem1  26002  lhop1lem  26007  dvcvx  26014  dvfsumle  26015  dvfsumleOLD  26016  dvfsumabs  26018  dvfsumlem4  26025  dvfsumrlim2  26028  ftc1a  26033  tdeglem4  26054  deg1pwle  26114  fta1blem  26165  aalioulem3  26331  aaliou2b  26338  ulmbdd  26396  ulmdvlem1  26398  itgulm  26406  pserdvlem2  26427  abelthlem3  26432  abelthlem5  26434  abelthlem6  26435  abelthlem7  26437  tanregt0  26536  argimlt0  26610  logdivlti  26617  logcnlem3  26641  logcnlem4  26642  logtayl  26657  logtayl2  26659  cxple2  26694  cxpcn3lem  26745  cxpaddle  26750  rtprmirr  26758  isosctrlem1  26816  atantayl  26935  efrlim  26967  efrlimOLD  26968  dfef2  26969  o1cxp  26973  cxp2lim  26975  divsqrtsumo1  26982  amgmlem  26988  logdifbnd  26992  emcllem7  27000  harmonicbnd4  27009  fsumharmonic  27010  lgamgulmlem2  27028  lgamgulmlem3  27029  lgamucov  27036  lgamcvg2  27053  gamcvg2  27058  ftalem2  27072  basellem2  27080  basellem5  27083  basellem9  27087  vma1  27164  sqff1o  27180  fsumfldivdiaglem  27187  chtub  27211  fsumvma2  27213  chpchtsum  27218  chpub  27219  logfaclbnd  27221  logfacbnd3  27222  logfacrlim  27223  logexprlim  27224  bcmono  27276  bposlem2  27284  bposlem5  27287  bposlem6  27288  lgsne0  27334  lgsquadlem1  27379  lgsquadlem2  27380  2sqblem  27430  2sqmod  27435  chebbnd1lem1  27468  chtppilimlem1  27472  chtppilimlem2  27473  chpchtlim  27478  rplogsumlem1  27483  dchrvmasumiflem1  27500  dchrisum0flblem2  27508  dchrisum0fno1  27510  dchrisum0lem2a  27516  dchrisum0lem3  27518  dirith  27528  mulog2sumlem1  27533  mulog2sumlem2  27534  log2sumbnd  27543  selberglem2  27545  logdivbnd  27555  selberg3lem1  27556  selberg4lem1  27559  pntrsumbnd2  27566  pntrlog2bndlem1  27576  pntrlog2bndlem5  27580  pntrlog2bndlem6  27582  pntpbnd1a  27584  pntpbnd1  27585  pntpbnd2  27586  pntibndlem3  27591  pntlemb  27596  pntlemn  27599  pntlemr  27601  pntlemj  27602  pntlemf  27604  pntlemo  27606  ostth2lem3  27634  ostth3  27637  addsuniflem  27989  sltp1d  28003  negsid  28028  negsunif  28042  mulsuniflem  28130  precsexlem9  28194  om2noseqlt  28260  n0sge0  28296  zscut  28348  addhalfcut  28374  footeq  28687  hlperpnel  28688  perpdragALT  28690  perpdrag  28691  colperp  28692  mideulem2  28697  opphllem  28698  opphllem3  28712  lmieu  28747  trgcopy  28767  sacgr  28794  acopyeu  28797  usgredgleordALT  29198  eucrctshift  30209  nvabs  30638  smcnlem  30663  ubthlem2  30837  minvecolem4  30846  htthlem  30883  normpyc  31112  nmophmi  31997  hstle  32196  hstles  32197  stlei  32206  f1rnen  32586  nnmulge  32696  fsumiunle  32778  wrdt2ind  32885  xrge0npcan  32971  gsumwrd2dccat  33016  trsp2cyc  33089  archirngz  33142  archiabllem1a  33144  archiabllem2a  33147  archiabllem2c  33148  elrgspnlem1  33192  elrgspn  33196  elrgspnsubrunlem2  33198  ornglmulle  33281  orngrmulle  33282  rprmasso  33494  q1pdir  33564  r1pquslmic  33572  drngdimgt0  33610  lbsdiflsp0  33618  fldextrspundgle  33669  fldext2rspun  33673  minplyirredlem  33694  madjusmdetlem2  33768  esumpinfval  34015  esumpinfsum  34019  esumpcvgval  34020  esum2d  34035  esumiun  34036  dya2icoseg  34220  omssubadd  34243  carsgsigalem  34258  carsggect  34261  carsgclctunlem3  34263  omsmeas  34266  eulerpartlems  34303  sgnmulsgn  34493  signsplypnf  34506  signsply0  34507  reprlt  34575  reprinfz1  34578  hgt750lemc  34603  hgt750lemf  34609  pthhashvtx  35074  resconn  35192  sinccvglem  35618  circum  35620  btwnxfr  35998  nn0prpwlem  36264  dnibndlem2  36421  unblimceq0  36449  irrdiff  37268  poimirlem7  37575  mblfinlem3  37607  mblfinlem4  37608  itg2addnclem3  37621  ftc1anc  37649  isbnd3  37732  cntotbnd  37744  bfp  37772  rrndstprj2  37779  1cvrjat  39418  3atlem1  39426  3atlem6  39431  llnmlplnN  39482  2llnjaN  39509  2lplnja  39562  dalem57  39672  dalawlem11  39824  dalawlem12  39825  lhp2lt  39944  lhpj1  39965  lhpm0atN  39972  4atexlemex2  40014  lautm  40037  cdleme17b  40230  cdleme20j  40261  cdleme30a  40321  cdlemg4c  40555  cdlemg17a  40604  cdlemg31c  40642  trljco  40683  cdlemk46  40891  dia2dimlem2  41008  cdlemm10N  41061  cdlemn10  41149  dihmeetlem1N  41233  dihglblem5apreN  41234  dihmeetlem15N  41264  mapdat  41610  lcmineqlem19  41989  lcmineqlem20  41990  aks4d1p1p5  42017  aks4d1p8d2  42027  aks4d1p8  42029  aks4d1p9  42030  hashscontpow  42064  metakunt29  42175  2xp3dxp2ge1d  42183  factwoffsmonot  42184  dvdsexpnn  42313  selvvvval  42540  evlselv  42542  mhphflem  42551  fltnlta  42618  3cubeslem1  42640  irrapxlem1  42778  irrapxlem4  42781  pell1qrgaplem  42829  pellfundglb  42841  rmspecfund  42865  monotoddzzfi  42899  rmynn  42913  jm2.24nn  42916  jm2.17c  42919  jm2.24  42920  acongeq  42940  jm2.20nn  42954  jm2.26lem3  42958  jm2.27a  42962  jm2.27c  42964  rmydioph  42971  jm3.1lem2  42975  frlmpwfi  43055  areaquad  43173  cantnf2  43283  rp-isfinite6  43476  frege129d  43721  leeq1d  44115  imo72b2lem0  44123  imo72b2  44130  cvgdvgrat  44277  radcnvrat  44278  hashnzfzclim  44286  isosctrlem1ALT  44899  cncmpmax  44982  iooabslt  45457  fmul01lt1lem2  45545  clim1fr1  45561  limcrecl  45589  climxrrelem  45709  liminflbuz2  45775  dvnprodlem1  45906  stoweidlem1  45961  stoweidlem11  45971  stoweidlem14  45974  stoweidlem24  45984  stoweidlem26  45986  wallispilem4  46028  wallispilem5  46029  stirlinglem1  46034  fourierdlem51  46117  fourierdlem65  46131  fouriersw  46191  2leaddle2  47256  sqrtpwpw2p  47471  lighneallem4a  47541  flnn0div2ge  48400  logbpw2m1  48434  functermclem  49108  amgmwlem  49317