Theorem breqtrrd 5114

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)

Hypotheses

Ref	Expression
breqtrrd.1	⊢ (𝜑 → 𝐴𝑅𝐵)
breqtrrd.2	⊢ (𝜑 → 𝐶 = 𝐵)

Assertion

Ref	Expression
breqtrrd	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem breqtrrd

Step	Hyp	Ref	Expression
1		breqtrrd.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		breqtrrd.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	2	eqcomd 2743	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	breqtrd 5112	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:  marypha1lem  9343  marypha2  9349  infsupprpr  9416  unxpwdom  9501  ttrcltr  9634  onadju  10113  nnadju  10117  cfss  10184  tskuni  10703  ltexnq  10895  lt2addmuld  12424  div4p1lem1div2  12429  nn0le2x  12488  mul2lt0rgt0  13044  prodge0ld  13049  ge2halflem1  13056  xrmax1  13124  xrmax2  13125  max1ALT  13135  qbtwnxr  13149  xleadd1a  13202  xlt2add  13209  xlesubadd  13212  xmulgt0  13232  xlemul1a  13237  xov1plusxeqvd  13448  uzsubsubfz  13497  fzctr  13591  subfzo0  13744  flflp1  13763  fldiv4lem1div2uz2  13792  ceilge  13801  modge0  13835  modlt  13836  modid  13852  m1modge3gt1  13877  modaddmodup  13893  sermono  13993  seqf1olem1  14000  seqf1olem2  14001  sqgt0  14085  sqge0  14095  leexp1a  14134  nnlesq  14164  expnbnd  14191  expmulnbnd  14194  discr1  14198  facwordi  14248  faclbnd5  14257  nfile  14318  hashdom  14338  hashgt23el  14383  fi1uzind  14466  brfi1indALT  14469  ccatdmss  14541  ccatws1n0  14592  swrds2  14899  cjmulge0  15105  resqrtcl  15212  absge0  15246  sqreulem  15319  amgm2  15329  rlimdm  15510  rlimge0  15540  reccn2  15556  climle  15599  climserle  15622  isercoll2  15628  iseraltlem1  15641  iseralt  15644  isumclim2  15717  isumclim3  15718  isumge0  15725  fsumless  15756  cvgcmp  15776  cvgcmpce  15778  abscvgcvg  15779  isumsup2  15808  isumltss  15810  climcndslem1  15811  climcnds  15813  supcvg  15818  harmonic  15821  expcnv  15826  explecnv  15827  cvgrat  15845  mertenslem1  15846  mertenslem2  15847  clim2div  15851  ntrivcvgtail  15862  iprodclim2  15961  iprodclim3  15962  efcvg  16047  ege2le3  16052  efaddlem  16055  eftlub  16073  effsumlt  16075  tanhlt1  16124  ef01bndlem  16148  sin02gt0  16156  rpnnen2lem4  16181  ruclem2  16196  ruclem3  16197  ruclem9  16202  iddvdsexp  16245  dvdsadd  16268  dvdsfac  16292  dvdsexp2im  16293  dvdsmod  16295  3dvds  16297  omoe  16330  sumeven  16353  divalglem1  16360  flodddiv4t2lthalf  16384  bitsfzo  16401  bitsmod  16402  bitscmp  16404  bitsinv1lem  16407  sadcaddlem  16423  sadadd3  16427  sadaddlem  16432  dvdssqim  16520  dvdsexpim  16521  dvdsmulgcd  16522  nn0seqcvgd  16536  dvdslcm  16564  lcmgcdlem  16572  dvdslcmf  16597  lcmfunsnlem2lem2  16605  mulgcddvds  16621  qredeq  16623  cncongr2  16634  sqnprm  16669  isprm6  16681  dvdszzq  16688  prmdvdsbc  16693  nonsq  16726  hashdvds  16742  prmdiv  16752  odzdvds  16763  pythagtriplem4  16787  pcpre1  16810  pcdvdsb  16837  pcz  16849  pcprmpw2  16850  pcaddlem  16856  pcadd  16857  pcadd2  16858  pcmpt  16860  pcmptdvds  16862  fldivp1  16865  pcfaclem  16866  pockthlem  16873  prmreclem1  16884  prmreclem3  16886  prmreclem5  16888  prmreclem6  16889  4sqlem6  16911  4sqlem8  16913  4sqlem11  16923  4sqlem12  16924  4sqlem14  16926  4sqlem16  16928  vdwlem3  16951  vdwlem9  16957  vdwlem10  16958  vdwlem12  16960  ramub1lem2  16995  prmgap  17027  prmgaplcm  17028  prmgapprmo  17030  mreexexd  17611  invfuc  17941  ple1  18391  chnub  18585  eqgen  19153  lagsubg  19167  pgpfi  19577  sylow2alem2  19590  sylow2a  19591  sylow3lem4  19602  efgsrel  19706  odadd1  19820  odadd2  19821  gexex  19825  lt6abl  19867  dprd2d2  20018  dmdprdpr  20023  ablfacrp2  20041  ablfac1c  20045  pgpfaclem1  20055  ablfac2  20063  fincygsubgodd  20086  omndmul2  20105  dvdsrmul1  20346  unitmulclb  20358  subrguss  20561  rhmsubcrngc  20642  abvres  20805  znfld  21556  znunit  21559  ofldchr  21572  frlmisfrlm  21844  ply1coefsupp  22278  evl1gsumadd  22339  matgsum  22418  pm2mpcl  22778  psmetxrge0  24294  isxmet2d  24308  mettri  24333  xmettri3  24334  mettri3  24335  xmetrtri2  24337  prdsxmetlem  24349  imasdsf1olem  24354  xblss2ps  24382  blss2ps  24384  blss2  24385  blssps  24405  blss  24406  prdsbl  24472  dscmet  24553  nmge0  24598  nmmtri  24603  tngngp3  24637  nlmvscnlem2  24666  nrginvrcnlem  24672  nmoix  24710  nmoleub  24712  blcvx  24779  xrsxmet  24791  opnreen  24813  xrge0tsms  24816  icopnfcnv  24925  xrhmeo  24929  lebnumii  24949  pcophtb  25012  pi1grplem  25032  nmoleub2lem  25097  ipcau2  25217  tcphcphlem1  25218  ipcau  25221  ipcnlem2  25227  rrxcph  25375  minveclem2  25409  minveclem3b  25411  pjthlem1  25420  pjthlem2  25421  ivthlem3  25436  ivth2  25438  ovolfsf  25454  ovolsslem  25467  ovollb2lem  25471  ovollb2  25472  ovolctb  25473  ovolfiniun  25484  ovolicc1  25499  ovolicc2lem4  25503  ovolicc2  25505  nulmbl2  25519  unmbl  25520  ioombl1lem4  25544  uniioombllem4  25569  uniioombllem6  25571  volivth  25590  vitalilem4  25594  itg1ge0  25669  itg1ge0a  25694  itg1lea  25695  itg1climres  25697  mbfi1fseqlem5  25702  itg2ub  25716  itg2seq  25725  itg2uba  25726  itg2splitlem  25731  itg2split  25732  itg2monolem3  25735  itg2mono  25736  itg2i1fseq2  25739  itg2addlem  25741  iblss  25788  itggt0  25827  dvferm2lem  25969  dvlip  25976  dvivthlem1  25991  dvfsumlem2  26010  dvfsumlem3  26011  ftc1lem4  26022  ply1divmo  26117  ply1remlem  26146  fta1glem2  26150  idomrootle  26154  ig1pdvds  26161  plyeq0lem  26191  plydiveu  26281  fta1lem  26290  vieta1lem2  26294  aaliou3lem2  26326  aaliou3lem8  26328  ulmcn  26383  mtest  26388  itgulm  26392  radcnvlem1  26397  radcnvlt1  26402  dvradcnv  26405  pserdvlem2  26412  abelthlem2  26416  abelthlem6  26420  abelthlem7  26422  abelthlem9  26424  tangtx  26488  sinq12gt0  26490  sineq0  26507  cosordlem  26513  tanord  26521  tanregt0  26522  logrnaddcl  26557  logcj  26589  argregt0  26593  argrege0  26594  argimgt0  26595  argimlt0  26596  logimul  26597  logneg2  26598  logdivlti  26603  divlogrlim  26618  logcnlem3  26627  logcnlem4  26628  dvlog2lem  26635  logtayl  26643  rpcxpcl  26659  cxpsqrtlem  26685  cxpaddle  26735  isosctrlem1  26801  asinlem3a  26853  asinlem3  26854  asinneg  26869  asinsinlem  26874  asinsin  26875  atanlogaddlem  26896  atanlogadd  26897  atanlogsublem  26898  atanlogsub  26899  atantan  26906  atanbndlem  26908  atantayl  26920  leibpi  26925  birthdaylem3  26936  areaf  26944  cxploglim  26961  jensenlem2  26971  jensen  26972  logdiflbnd  26978  harmonicbnd4  26994  fsumharmonic  26995  zetacvg  26998  lgamgulmlem2  27013  lgamgulmlem3  27014  lgamcvg2  27038  wilthlem2  27052  wilthimp  27055  ftalem1  27056  ftalem2  27057  ftalem5  27060  basellem6  27069  basellem8  27071  basellem9  27072  chtge0  27095  chtublem  27194  logexprlim  27208  perfectlem1  27212  bcmax  27261  bposlem1  27267  bposlem2  27268  bposlem6  27272  bposlem7  27273  lgsdilem2  27316  lgsqrlem4  27332  lgsquadlem1  27363  2lgsoddprmlem2  27392  2sqlem3  27403  2sqlem8  27409  2sqblem  27414  2sqmod  27419  chebbnd1lem2  27453  chtppilimlem1  27456  chtppilim  27458  chto1ub  27459  vmadivsum  27465  rplogsumlem1  27467  rplogsumlem2  27468  dchrisum0lem1a  27469  rpvmasumlem  27470  dchrisumlem1  27472  dchrisumlem2  27473  dchrvmasumlem2  27481  dchrisum0flblem1  27491  dchrisum0flblem2  27492  dchrisum0lem1b  27498  dchrisum0lem1  27499  dchrisum0lem2a  27500  dchrisum0lem3  27502  dchrisum0  27503  mudivsum  27513  mulogsumlem  27514  mulog2sumlem1  27517  mulog2sumlem2  27518  2vmadivsumlem  27523  chpdifbndlem1  27536  selberg3lem1  27540  selberg4lem1  27543  pntrlog2bndlem1  27560  pntrlog2bndlem2  27561  pntrlog2bndlem3  27562  pntrlog2bndlem4  27563  pntpbnd1a  27568  pntpbnd1  27569  pntpbnd2  27570  pntibndlem2  27574  pntibndlem3  27575  pntlemd  27577  pntlemc  27578  pntlemb  27580  pntlemg  27581  pntlemh  27582  pntlemr  27585  pntlemf  27588  pntlemo  27590  abvcxp  27598  ostth2lem1  27601  padicabv  27613  ostth2lem2  27617  ostth2lem3  27618  ostth2lem4  27619  ostth2  27620  ostth3  27621  nodense  27676  nogt01o  27680  nosupbnd2lem1  27699  noetasuplem3  27719  maxs1  27753  maxs2  27754  eqcuts3  27816  cofcutr  27936  cofcutrtime  27939  addsuniflem  28013  negsunif  28067  sltmuls2  28160  precsexlem11  28229  abssge0  28257  leabss  28260  oncutlt  28276  om2noseqlt  28311  zsoring  28421  expsgt0  28449  halfcut  28470  addhalfcut  28471  bdayfinbndlem1  28479  elreno2  28507  tgcgr4  28619  legso  28687  krippenlem  28778  midex  28825  oppperpex  28841  ttgcontlem1  28973  axpaschlem  29029  axcontlem8  29060  upgrex  29181  nbfusgrlevtxm1  29466  finsumvtxdgeven  29642  wwlksnextproplem3  30000  clwlkclwwlk2  30094  clwlkclwwlkfolem  30098  clwwlkndivn  30171  ex-ind-dvds  30552  nvabs  30764  nmooge0  30859  nmoolb  30863  siii  30945  minvecolem2  30967  minvecolem4  30972  minvecolem5  30973  hlipgt0  31006  normge0  31218  normpyc  31238  pjhthlem1  31483  pjige0i  31782  nmoplb  31999  nmfnlb  32016  branmfn  32197  pjssdif2i  32266  stlei  32332  xlt2addrd  32853  eliccelico  32871  elicoelioo  32872  bcm1n  32889  fsumiunle  32923  sgnmul  32929  nexple  32938  expevenpos  32940  pfxlsw2ccat  33031  wrdt2ind  33034  xrge0tsmsd  33155  gsumwrd2dccatlem  33159  psgnfzto1stlem  33182  cycpmco2lem4  33211  cycpmco2lem5  33212  cyc3conja  33239  archirngz  33271  archiabllem2c  33277  rprmasso2  33607  rprmirred  33612  1arithufdlem3  33627  vietadeg1  33743  lbslelsp  33763  fedgmullem2  33796  extdggt0  33823  evls1fldgencl  33836  fldextrspunlem1  33841  extdgfialglem1  33858  algextdeglem8  33890  rtelextdg2lem  33892  cos9thpiminplylem1  33948  cos9thpiminplylem2  33949  madjusmdetlem2  33994  locfinreflem  34006  xrge0iifiso  34101  gsumesum  34225  esumcst  34229  esumpcvgval  34244  esumcvg  34252  esumiun  34260  measssd  34381  measunl  34382  omssubadd  34466  carsgclctunlem3  34486  pmeasmono  34490  sibfof  34506  oddpwdc  34520  eulerpartlemgc  34528  iwrdsplit  34553  ballotlemsgt1  34677  ballotlemsel1i  34679  signsply0  34717  signstfvc  34740  signsvtp  34749  signsvfpn  34751  fdvposlt  34765  fdvneggt  34766  fdvnegge  34768  logdivsqrle  34816  hgt750lemf  34819  tgoldbachgtde  34826  swrdwlk  35331  subfaclim  35392  erdszelem7  35401  erdszelem8  35402  cvmliftlem2  35490  snmlff  35533  sinccvglem  35876  climlec3  35938  faclim  35950  fnejoin1  36572  poimirlem12  37975  poimirlem17  37980  poimirlem19  37982  poimirlem20  37983  poimirlem23  37986  poimirlem28  37991  broucube  37997  mblfinlem2  38001  mblfinlem3  38002  mblfinlem4  38003  ismblfin  38004  itg2addnclem  38014  itg2addnclem3  38016  itg2gt0cn  38018  itggt0cn  38033  ftc1anclem5  38040  ftc1anclem7  38042  ftc1anclem8  38043  isbnd3  38127  ssbnd  38131  heiborlem8  38161  bfplem2  38166  rrncmslem  38175  rrnequiv  38178  rrntotbnd  38179  lcv1  39509  lsatcv0eq  39515  lsatcvat3  39520  cvlsupr2  39811  hlatlej2  39844  cvrval4N  39882  cvratlem  39889  atcvr0eq  39894  2atlt  39907  atbtwnex  39916  athgt  39924  1cvrat  39944  ps-1  39945  hlatexch3N  39948  hlatexch4  39949  3atlem2  39952  atcvrlln2  39987  lplnexllnN  40032  4atlem3a  40065  4atlem10b  40073  4atlem11b  40076  4atlem12b  40079  2lplnja  40087  dalemply  40122  dalemsly  40123  dalem1  40127  dalem6  40136  dalem7  40137  dalem-cly  40139  dalem11  40142  dalem12  40143  dalem16  40147  dalem17  40148  dalem38  40178  dalem44  40184  dalem61  40201  lnatexN  40247  lncvrat  40250  lncmp  40251  paddasslem2  40289  dalawlem3  40341  dalawlem6  40344  dalawlem11  40349  lhpmcvr  40491  lhp2atne  40502  lhp2at0ne  40504  lautj  40561  trlval4  40656  cdlemc2  40660  cdlemc5  40663  cdleme3b  40697  cdleme11c  40729  cdleme19a  40771  cdleme20j  40786  cdleme22f  40814  cdleme23c  40819  cdleme26f2ALTN  40832  cdleme26f2  40833  cdleme35fnpq  40917  cdleme48bw  40970  cdlemg10a  41108  cdlemg11b  41110  cdlemg17g  41135  cdlemg18c  41148  cdlemi1  41286  cdlemk52  41422  dia2dimlem1  41532  dihord1  41686  dihjatcclem4  41889  lcmineqlem15  42504  lcmineqlem19  42508  lcmineqlem22  42511  aks4d1lem1  42523  aks4d1p1p4  42532  aks4d1p1p5  42536  aks4d1p2  42538  aks4d1p3  42539  aks4d1p6  42542  aks4d1p7d1  42543  aks4d1p7  42544  aks4d1p8  42548  aks4d1p9  42549  aks6d1c1p6  42575  aks6d1c1  42577  aks6d1c2  42591  sticksstones7  42613  aks6d1c7lem1  42641  unitscyglem4  42659  dvdsexpnn0  42788  prjspner01  43080  flt4lem5  43105  fltnltalem  43117  fltnlta  43118  3cubeslem1  43138  eldioph2lem1  43214  lzenom  43224  irrapxlem1  43276  irrapxlem4  43279  irrapxlem5  43280  pell14qrgt0  43313  pell1qrge1  43324  pell1qrgap  43328  pellfundge  43336  pellfundex  43340  pellfund14  43352  rmspecsqrtnq  43360  rmxypos  43401  ltrmynn0  43402  ltrmxnn0  43403  jm2.24nn  43413  jm2.17b  43415  jm2.17c  43416  jm2.24  43417  congadd  43420  congsym  43422  congneg  43423  congid  43425  mzpcong  43426  acongrep  43434  acongeq  43437  jm2.18  43442  jm2.19  43447  jm2.23  43450  jm2.25  43453  jm2.26lem3  43455  jm2.15nn0  43457  jm2.16nn0  43458  jm2.27a  43459  jm2.27c  43461  jm3.1lem1  43471  idomsubgmo  43647  sqrtcval  44094  inductionexd  44608  imo72b2lem0  44618  imo72b2  44625  dvgrat  44765  radcnvrat  44767  binomcxplemnn0  44802  binomcxplemnotnn0  44809  cncmpmax  45489  rnmptlb  45698  zltlesub  45744  infxrpnf  45900  xrpnf  45939  fmul01  46036  fmul01lt1lem1  46040  climdivf  46068  sumnnodd  46086  climinf2lem  46160  limsup10exlem  46226  climliminf  46260  dfxlim2v  46301  xlimliminflimsup  46316  dvdivbd  46377  volge0  46415  stoweidlem1  46455  stoweidlem16  46470  stoweidlem18  46472  stoweidlem24  46478  stoweidlem26  46480  stoweidlem36  46490  stoweidlem38  46492  stoweidlem41  46495  stoweidlem42  46496  stoweidlem44  46498  stoweidlem45  46499  stoweidlem48  46502  stoweidlem62  46516  wallispilem5  46523  stirlinglem1  46528  stirlinglem5  46532  stirlinglem7  46534  stirlinglem8  46535  stirlinglem9  46536  stirlinglem11  46538  fourierdlem4  46565  fourierdlem10  46571  fourierdlem37  46598  fourierdlem47  46607  fourierdlem72  46632  fourierdlem74  46634  fourierdlem79  46639  fourierdlem82  46642  fourierdlem89  46649  fourierdlem91  46651  fourierdlem93  46653  fourierdlem103  46663  fourierdlem104  46664  fourierdlem112  46672  etransclem24  46712  etransclem25  46713  etransclem28  46716  etransclem37  46725  etransclem38  46726  etransclem44  46732  meaiuninc3v  46938  vonicclem1  47137  pimconstlt0  47155  smfsuplem1  47265  chnerlem1  47336  rlimdmafv  47645  rlimdmafv2  47726  2elfz2melfz  47786  2timesltsq  47846  muldvdsfacgt  47854  iccpartgtprec  47900  iccpartlt  47904  iccpartgtl  47906  sqrtpwpw2p  48021  fmtnodvds  48027  goldbachthlem1  48028  lighneallem4a  48091  nprmdvdsfacm1lem1  48103  perfectALTVlem1  48217  uhgrimgrlim  48483  cznnring  48758  altgsumbcALT  48849  expnegico01  49014  flnn0div2ge  49029  rege1logbrege0  49054  fllogbd  49056  nnpw2blen  49076  nnolog2flm1  49086  dignn0ldlem  49098  dignn0flhalflem1  49111  dignn0flhalflem2  49112  eenglngeehlnmlem2  49234  itsclc0yqsol  49260  2itscp  49277  itscnhlinecirc02plem1  49278  itscnhlinecirc02plem2  49279  inlinecirc02p  49283