Theorem eqbrtrrd 5110

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

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

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087

This theorem is referenced by:  dftpos4  8189  dif1en  9090  fodomfi  9216  fodomfiOLD  9234  fmptssfisupp  9301  resfifsupp  9304  cnfcom2lem  9616  dmttrcl  9636  ttrclselem2  9641  ficardadju  10116  enfin1ai  10300  pwcfsdom  10500  fpwwe2lem6  10553  fpwwe2  10560  canthp1lem1  10569  1nqenq  10879  prlem936  10964  lemulge11  12012  supaddc  12117  supmul1  12119  mul2lt0llt0  13042  mul2lt0lgt0  13043  xaddge0  13204  xadddi2  13243  ltexp2a  14122  leexp2a  14128  nnlesq  14161  digit1  14193  faclbnd4lem1  14249  faclbnd6  14255  facavg  14257  prsshashgt1  14366  nehash2  14430  abs3dif  15288  abs2dif  15289  limsupgre  15437  rlimclim1  15501  rlimuni  15506  rlimres2  15517  rlimcn1  15544  rlimcn1b  15545  recn2  15557  imcn2  15558  rlimo1  15573  o1rlimmul  15575  iserex  15613  isercoll  15624  caucvgrlem2  15631  caucvgr  15632  iseraltlem3  15640  summolem2a  15671  fsumge1  15754  o1fsum  15770  isumrpcl  15802  climcnds  15810  harmonic  15818  mertenslem1  15843  prodmolem2a  15893  ege2le3  16049  efgt1p2  16075  efgt1p  16076  eirrlem  16165  rpnnen2lem11  16185  fsumdvds  16271  bitsfzo  16398  bitsmod  16399  bitscmp  16401  mulgcd  16511  dvdssqlem  16529  nn0seqcvgd  16533  mulgcddvds  16618  rpdvds  16623  qden1elz  16721  phimullem  16743  hashgcdlem  16752  hashgcdeq  16754  pcdvdstr  16841  pockthg  16871  prmreclem1  16881  4sqlem11  16920  ramub1lem1  16991  ramub1lem2  16992  mreexexlem4d  17607  sscid  17785  latmlej21  18440  latmlej22  18441  lubel  18474  efginvrel1  19697  odadd2  19818  odadd  19819  gexexlem  19821  cyggex2  19866  ablfacrplem  20036  ablfac1c  20042  ablfac1eu  20044  pgpfac1lem3a  20047  isabvd  20783  ornglmulle  20838  orngrmulle  20839  mptscmfsuppd  20917  znrrg  21558  frlmphl  21774  frlmup1  21791  f1linds  21818  psdmplcl  22141  chcoeffeqlem  22863  lmcn2  23627  metrtri  24335  imasdsf1olem  24351  stdbdxmet  24493  nrmmetd  24552  nmmtri  24600  nlmvscnlem2  24663  blcvx  24776  recld2  24793  zdis  24795  opnreen  24810  cnheibor  24935  lebnumlem3  24943  nmoleub2lem3  25095  nmoleub2lem2  25096  nmoleub3  25099  ipcnlem2  25224  cmetcaulem  25268  nglmle  25282  cncmet  25302  csbren  25379  trirn  25380  minveclem4  25412  ovoliunlem1  25482  ovoliun2  25486  ovolscalem1  25493  ovolicopnf  25504  voliunlem2  25531  volsup  25536  ioorcl2  25552  uniiccvol  25560  uniioombllem4  25566  i1fd  25661  mbfi1fseqlem4  25698  itg2const2  25721  itg2eqa  25725  itg2split  25729  itg2i1fseqle  25734  itg2cnlem2  25742  dvcnv  25957  dveflem  25959  dvferm1lem  25964  dvlip2  25975  c1liplem1  25976  dvivthlem1  25988  lhop1lem  25993  dvcvx  26000  dvfsumle  26001  dvfsumabs  26003  dvfsumlem4  26009  dvfsumrlim2  26012  ftc1a  26017  tdeglem4  26038  deg1pwle  26098  fta1blem  26149  aalioulem3  26314  aaliou2b  26321  ulmbdd  26379  ulmdvlem1  26381  itgulm  26389  pserdvlem2  26409  abelthlem3  26414  abelthlem5  26416  abelthlem6  26417  abelthlem7  26419  tanregt0  26519  argimlt0  26593  logdivlti  26600  logcnlem3  26624  logcnlem4  26625  logtayl  26640  logtayl2  26642  cxple2  26677  cxpcn3lem  26727  cxpaddle  26732  rtprmirr  26740  isosctrlem1  26798  atantayl  26917  efrlim  26949  efrlimOLD  26950  dfef2  26951  o1cxp  26955  cxp2lim  26957  divsqrtsumo1  26964  amgmlem  26970  logdifbnd  26974  emcllem7  26982  harmonicbnd4  26991  fsumharmonic  26992  lgamgulmlem2  27010  lgamgulmlem3  27011  lgamucov  27018  lgamcvg2  27035  gamcvg2  27040  ftalem2  27054  basellem2  27062  basellem5  27065  basellem9  27069  vma1  27146  sqff1o  27162  fsumfldivdiaglem  27169  chtub  27192  fsumvma2  27194  chpchtsum  27199  chpub  27200  logfaclbnd  27202  logfacbnd3  27203  logfacrlim  27204  logexprlim  27205  bcmono  27257  bposlem2  27265  bposlem5  27268  bposlem6  27269  lgsne0  27315  lgsquadlem1  27360  lgsquadlem2  27361  2sqblem  27411  2sqmod  27416  chebbnd1lem1  27449  chtppilimlem1  27453  chtppilimlem2  27454  chpchtlim  27459  rplogsumlem1  27464  dchrvmasumiflem1  27481  dchrisum0flblem2  27489  dchrisum0fno1  27491  dchrisum0lem2a  27497  dchrisum0lem3  27499  dirith  27509  mulog2sumlem1  27514  mulog2sumlem2  27515  log2sumbnd  27524  selberglem2  27526  logdivbnd  27536  selberg3lem1  27537  selberg4lem1  27540  pntrsumbnd2  27547  pntrlog2bndlem1  27557  pntrlog2bndlem5  27561  pntrlog2bndlem6  27563  pntpbnd1a  27565  pntpbnd1  27566  pntpbnd2  27567  pntibndlem3  27572  pntlemb  27577  pntlemn  27580  pntlemr  27582  pntlemj  27583  pntlemf  27585  pntlemo  27587  ostth2lem3  27615  ostth3  27618  addsuniflem  28010  ltsp1d  28024  negsid  28050  negsunif  28064  negleft  28067  mulsuniflem  28158  precsexlem9  28224  n0sge0  28347  zcuts  28416  halfcut  28467  addhalfcut  28468  pw2cut2  28471  bdayfinbndlem1  28476  footeq  28809  hlperpnel  28810  perpdragALT  28812  perpdrag  28813  colperp  28814  mideulem2  28819  opphllem  28820  opphllem3  28834  lmieu  28869  trgcopy  28889  sacgr  28916  acopyeu  28919  usgredgleordALT  29320  eucrctshift  30331  nvabs  30761  smcnlem  30786  ubthlem2  30960  minvecolem4  30969  htthlem  31006  normpyc  31235  nmophmi  32120  hstle  32319  hstles  32320  stlei  32329  f1rnen  32719  nnmulge  32830  fsumiunle  32920  sgnmulsgn  32933  wrdt2ind  33031  xrge0npcan  33098  gsumwrd2dccat  33157  trsp2cyc  33202  archirngz  33268  archiabllem1a  33270  archiabllem2a  33273  archiabllem2c  33274  elrgspnlem1  33321  elrgspn  33325  elrgspnsubrunlem2  33327  rprmasso  33603  q1pdir  33681  r1pquslmic  33689  evlextv  33704  mplvrpmga  33707  mplvrpmrhm  33709  drngdimgt0  33781  lbsdiflsp0  33789  fldextrspundgle  33841  fldext2rspun  33845  minplyirredlem  33873  madjusmdetlem2  33991  esumpinfval  34236  esumpinfsum  34240  esumpcvgval  34241  esum2d  34256  esumiun  34257  dya2icoseg  34440  omssubadd  34463  carsgsigalem  34478  carsggect  34481  carsgclctunlem3  34483  omsmeas  34486  eulerpartlems  34523  signsplypnf  34713  signsply0  34714  reprlt  34782  reprinfz1  34785  hgt750lemc  34810  hgt750lemf  34816  pthhashvtx  35329  resconn  35447  sinccvglem  35873  circum  35875  btwnxfr  36257  nn0prpwlem  36523  dnibndlem2  36758  unblimceq0  36786  irrdiff  37659  poimirlem7  37965  mblfinlem3  37997  mblfinlem4  37998  itg2addnclem3  38011  ftc1anc  38039  isbnd3  38122  cntotbnd  38134  bfp  38162  rrndstprj2  38169  1cvrjat  39938  3atlem1  39946  3atlem6  39951  llnmlplnN  40002  2llnjaN  40029  2lplnja  40082  dalem57  40192  dalawlem11  40344  dalawlem12  40345  lhp2lt  40464  lhpj1  40485  lhpm0atN  40492  4atexlemex2  40534  lautm  40557  cdleme17b  40750  cdleme20j  40781  cdleme30a  40841  cdlemg4c  41075  cdlemg17a  41124  cdlemg31c  41162  trljco  41203  cdlemk46  41411  dia2dimlem2  41528  cdlemm10N  41581  cdlemn10  41669  dihmeetlem1N  41753  dihglblem5apreN  41754  dihmeetlem15N  41784  mapdat  42130  lcmineqlem19  42503  lcmineqlem20  42504  aks4d1p1p5  42531  aks4d1p8d2  42541  aks4d1p8  42543  aks4d1p9  42544  hashscontpow  42578  dvdsexpnn  42782  mullt0b1d  42945  selvvvval  43035  evlselv  43037  mhphflem  43046  fltnlta  43113  3cubeslem1  43133  irrapxlem1  43271  irrapxlem4  43274  pell1qrgaplem  43322  pellfundglb  43334  rmspecfund  43358  monotoddzzfi  43391  rmynn  43405  jm2.24nn  43408  jm2.17c  43411  jm2.24  43412  acongeq  43432  jm2.20nn  43446  jm2.26lem3  43450  jm2.27a  43454  jm2.27c  43456  rmydioph  43463  jm3.1lem2  43467  frlmpwfi  43547  areaquad  43665  cantnf2  43774  rp-isfinite6  43966  frege129d  44211  leeq1d  44605  imo72b2lem0  44613  imo72b2  44620  cvgdvgrat  44761  radcnvrat  44762  hashnzfzclim  44770  isosctrlem1ALT  45381  cncmpmax  45484  iooabslt  45950  fmul01lt1lem2  46036  clim1fr1  46052  limcrecl  46080  climxrrelem  46198  liminflbuz2  46264  dvnprodlem1  46395  stoweidlem1  46450  stoweidlem11  46460  stoweidlem14  46463  stoweidlem24  46473  stoweidlem26  46475  wallispilem4  46517  wallispilem5  46518  stirlinglem1  46523  fourierdlem51  46606  fourierdlem65  46620  fouriersw  46680  2leaddle2  47761  2timesltsqm1  47842  sqrtpwpw2p  48016  lighneallem4a  48086  flnn0div2ge  49024  logbpw2m1  49058  functermclem  49997  amgmwlem  50292