Theorem breqtrrd 5171

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144

This theorem is referenced by:  marypha1lem  9473  marypha2  9479  infsupprpr  9544  unxpwdom  9629  ttrcltr  9756  onadju  10234  nnadju  10238  cfss  10305  tskuni  10823  ltexnq  11015  lt2addmuld  12516  div4p1lem1div2  12521  nn0le2x  12580  mul2lt0rgt0  13138  prodge0ld  13143  ge2halflem1  13150  xrmax1  13217  xrmax2  13218  max1ALT  13228  qbtwnxr  13242  xleadd1a  13295  xlt2add  13302  xlesubadd  13305  xmulgt0  13325  xlemul1a  13330  xov1plusxeqvd  13538  uzsubsubfz  13586  fzctr  13680  subfzo0  13828  flflp1  13847  fldiv4lem1div2uz2  13876  ceilge  13885  modge0  13919  modlt  13920  modid  13936  m1modge3gt1  13959  modaddmodup  13975  sermono  14075  seqf1olem1  14082  seqf1olem2  14083  sqgt0  14166  sqge0  14176  leexp1a  14215  nnlesq  14244  expnbnd  14271  expmulnbnd  14274  discr1  14278  facwordi  14328  faclbnd5  14337  nfile  14398  hashdom  14418  hashgt23el  14463  fi1uzind  14546  brfi1indALT  14549  ccatws1n0  14670  swrds2  14979  cjmulge0  15185  resqrtcl  15292  absge0  15326  sqreulem  15398  amgm2  15408  rlimdm  15587  rlimge0  15617  reccn2  15633  climle  15676  climserle  15699  isercoll2  15705  iseraltlem1  15718  iseralt  15721  isumclim2  15794  isumclim3  15795  isumge0  15802  fsumless  15832  cvgcmp  15852  cvgcmpce  15854  abscvgcvg  15855  isumsup2  15882  isumltss  15884  climcndslem1  15885  climcnds  15887  supcvg  15892  harmonic  15895  expcnv  15900  explecnv  15901  cvgrat  15919  mertenslem1  15920  mertenslem2  15921  clim2div  15925  ntrivcvgtail  15936  iprodclim2  16035  iprodclim3  16036  efcvg  16121  ege2le3  16126  efaddlem  16129  eftlub  16145  effsumlt  16147  tanhlt1  16196  ef01bndlem  16220  sin02gt0  16228  rpnnen2lem4  16253  ruclem2  16268  ruclem3  16269  ruclem9  16274  iddvdsexp  16317  dvdsadd  16339  dvdsfac  16363  dvdsexp2im  16364  dvdsmod  16366  3dvds  16368  omoe  16401  sumeven  16424  divalglem1  16431  flodddiv4t2lthalf  16455  bitsfzo  16472  bitsmod  16473  bitscmp  16475  bitsinv1lem  16478  sadcaddlem  16494  sadadd3  16498  sadaddlem  16503  dvdssqim  16591  dvdsexpim  16592  dvdsmulgcd  16593  nn0seqcvgd  16607  dvdslcm  16635  lcmgcdlem  16643  dvdslcmf  16668  lcmfunsnlem2lem2  16676  mulgcddvds  16692  qredeq  16694  cncongr2  16705  sqnprm  16739  isprm6  16751  dvdszzq  16758  prmdvdsbc  16763  nonsq  16796  hashdvds  16812  prmdiv  16822  odzdvds  16833  pythagtriplem4  16857  pcpre1  16880  pcdvdsb  16907  pcz  16919  pcprmpw2  16920  pcaddlem  16926  pcadd  16927  pcadd2  16928  pcmpt  16930  pcmptdvds  16932  fldivp1  16935  pcfaclem  16936  pockthlem  16943  prmreclem1  16954  prmreclem3  16956  prmreclem5  16958  prmreclem6  16959  4sqlem6  16981  4sqlem8  16983  4sqlem11  16993  4sqlem12  16994  4sqlem14  16996  4sqlem16  16998  vdwlem3  17021  vdwlem9  17027  vdwlem10  17028  vdwlem12  17030  ramub1lem2  17065  prmgap  17097  prmgaplcm  17098  prmgapprmo  17100  mreexexd  17691  invfuc  18022  ple1  18475  eqgen  19199  lagsubg  19213  pgpfi  19623  sylow2alem2  19636  sylow2a  19637  sylow3lem4  19648  efgsrel  19752  odadd1  19866  odadd2  19867  gexex  19871  lt6abl  19913  dprd2d2  20064  dmdprdpr  20069  ablfacrp2  20087  ablfac1c  20091  pgpfaclem1  20101  ablfac2  20109  fincygsubgodd  20132  dvdsrmul1  20369  unitmulclb  20381  subrguss  20587  rhmsubcrngc  20668  abvres  20832  znfld  21579  znunit  21582  frlmisfrlm  21868  ply1coefsupp  22301  evl1gsumadd  22362  matgsum  22443  pm2mpcl  22803  psmetxrge0  24323  isxmet2d  24337  mettri  24362  xmettri3  24363  mettri3  24364  xmetrtri2  24366  prdsxmetlem  24378  imasdsf1olem  24383  xblss2ps  24411  blss2ps  24413  blss2  24414  blssps  24434  blss  24435  prdsbl  24504  dscmet  24585  nmge0  24630  nmmtri  24635  tngngp3  24677  nlmvscnlem2  24706  nrginvrcnlem  24712  nmoix  24750  nmoleub  24752  blcvx  24819  xrsxmet  24831  opnreen  24853  xrge0tsms  24856  icopnfcnv  24973  xrhmeo  24977  lebnumii  24998  pcophtb  25062  pi1grplem  25082  nmoleub2lem  25147  ipcau2  25268  tcphcphlem1  25269  ipcau  25272  ipcnlem2  25278  rrxcph  25426  minveclem2  25460  minveclem3b  25462  pjthlem1  25471  pjthlem2  25472  ivthlem3  25488  ivth2  25490  ovolfsf  25506  ovolsslem  25519  ovollb2lem  25523  ovollb2  25524  ovolctb  25525  ovolfiniun  25536  ovolicc1  25551  ovolicc2lem4  25555  ovolicc2  25557  nulmbl2  25571  unmbl  25572  ioombl1lem4  25596  uniioombllem4  25621  uniioombllem6  25623  volivth  25642  vitalilem4  25646  itg1ge0  25721  itg1ge0a  25746  itg1lea  25747  itg1climres  25749  mbfi1fseqlem5  25754  itg2ub  25768  itg2seq  25777  itg2uba  25778  itg2splitlem  25783  itg2split  25784  itg2monolem3  25787  itg2mono  25788  itg2i1fseq2  25791  itg2addlem  25793  iblss  25840  itggt0  25879  dvferm2lem  26024  dvlip  26032  dvivthlem1  26047  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsumlem3  26069  ftc1lem4  26080  ply1divmo  26175  ply1remlem  26204  fta1glem2  26208  idomrootle  26212  ig1pdvds  26219  plyeq0lem  26249  plydiveu  26340  fta1lem  26349  vieta1lem2  26353  aaliou3lem2  26385  aaliou3lem8  26387  ulmcn  26442  mtest  26447  itgulm  26451  radcnvlem1  26456  radcnvlt1  26461  dvradcnv  26464  pserdvlem2  26472  abelthlem2  26476  abelthlem6  26480  abelthlem7  26482  abelthlem9  26484  tangtx  26547  sinq12gt0  26549  sineq0  26566  cosordlem  26572  tanord  26580  tanregt0  26581  logrnaddcl  26616  logcj  26648  argregt0  26652  argrege0  26653  argimgt0  26654  argimlt0  26655  logimul  26656  logneg2  26657  logdivlti  26662  divlogrlim  26677  logcnlem3  26686  logcnlem4  26687  dvlog2lem  26694  logtayl  26702  rpcxpcl  26718  cxpsqrtlem  26744  cxpaddle  26795  isosctrlem1  26861  asinlem3a  26913  asinlem3  26914  asinneg  26929  asinsinlem  26934  asinsin  26935  atanlogaddlem  26956  atanlogadd  26957  atanlogsublem  26958  atanlogsub  26959  atantan  26966  atanbndlem  26968  atantayl  26980  leibpi  26985  birthdaylem3  26996  areaf  27004  cxploglim  27021  jensenlem2  27031  jensen  27032  logdiflbnd  27038  harmonicbnd4  27054  fsumharmonic  27055  zetacvg  27058  lgamgulmlem2  27073  lgamgulmlem3  27074  lgamcvg2  27098  wilthlem2  27112  wilthimp  27115  ftalem1  27116  ftalem2  27117  ftalem5  27120  basellem6  27129  basellem8  27131  basellem9  27132  chtge0  27155  chtublem  27255  logexprlim  27269  perfectlem1  27273  bcmax  27322  bposlem1  27328  bposlem2  27329  bposlem6  27333  bposlem7  27334  lgsdilem2  27377  lgsqrlem4  27393  lgsquadlem1  27424  2lgsoddprmlem2  27453  2sqlem3  27464  2sqlem8  27470  2sqblem  27475  2sqmod  27480  chebbnd1lem2  27514  chtppilimlem1  27517  chtppilim  27519  chto1ub  27520  vmadivsum  27526  rplogsumlem1  27528  rplogsumlem2  27529  dchrisum0lem1a  27530  rpvmasumlem  27531  dchrisumlem1  27533  dchrisumlem2  27534  dchrvmasumlem2  27542  dchrisum0flblem1  27552  dchrisum0flblem2  27553  dchrisum0lem1b  27559  dchrisum0lem1  27560  dchrisum0lem2a  27561  dchrisum0lem3  27563  dchrisum0  27564  mudivsum  27574  mulogsumlem  27575  mulog2sumlem1  27578  mulog2sumlem2  27579  2vmadivsumlem  27584  chpdifbndlem1  27597  selberg3lem1  27601  selberg4lem1  27604  pntrlog2bndlem1  27621  pntrlog2bndlem2  27622  pntrlog2bndlem3  27623  pntrlog2bndlem4  27624  pntpbnd1a  27629  pntpbnd1  27630  pntpbnd2  27631  pntibndlem2  27635  pntibndlem3  27636  pntlemd  27638  pntlemc  27639  pntlemb  27641  pntlemg  27642  pntlemh  27643  pntlemr  27646  pntlemf  27649  pntlemo  27651  abvcxp  27659  ostth2lem1  27662  padicabv  27674  ostth2lem2  27678  ostth2lem3  27679  ostth2lem4  27680  ostth2  27681  ostth3  27682  nodense  27737  nogt01o  27741  nosupbnd2lem1  27760  noetasuplem3  27780  maxs1  27810  maxs2  27811  cofcutr  27958  cofcutrtime  27961  addsuniflem  28034  negsunif  28087  ssltmul2  28174  precsexlem11  28241  abssge0  28269  sleabs  28272  om2noseqlt  28305  expsgt0  28415  halfcut  28416  addhalfcut  28419  tgcgr4  28539  legso  28607  krippenlem  28698  midex  28745  oppperpex  28761  ttgcontlem1  28899  axpaschlem  28955  axcontlem8  28986  upgrex  29109  nbfusgrlevtxm1  29394  finsumvtxdgeven  29570  wwlksnextproplem3  29931  clwlkclwwlk2  30022  clwlkclwwlkfolem  30026  clwwlkndivn  30099  ex-ind-dvds  30480  nvabs  30691  nmooge0  30786  nmoolb  30790  siii  30872  minvecolem2  30894  minvecolem4  30899  minvecolem5  30900  hlipgt0  30933  normge0  31145  normpyc  31165  pjhthlem1  31410  pjige0i  31709  nmoplb  31926  nmfnlb  31943  branmfn  32124  pjssdif2i  32193  stlei  32259  xlt2addrd  32762  eliccelico  32779  elicoelioo  32780  bcm1n  32797  fsumiunle  32831  nexple  32833  ccatdmss  32934  pfxlsw2ccat  32935  wrdt2ind  32938  chnub  33002  xrge0tsmsd  33065  gsumwrd2dccatlem  33069  omndmul2  33089  psgnfzto1stlem  33120  cycpmco2lem4  33149  cycpmco2lem5  33150  cyc3conja  33177  archirngz  33196  archiabllem2c  33202  ofldchr  33344  rprmasso2  33554  rprmirred  33559  1arithufdlem3  33574  lbslelsp  33648  fedgmullem2  33681  extdggt0  33708  evls1fldgencl  33720  fldextrspunlem1  33725  algextdeglem8  33765  rtelextdg2lem  33767  madjusmdetlem2  33827  locfinreflem  33839  xrge0iifiso  33934  gsumesum  34060  esumcst  34064  esumpcvgval  34079  esumcvg  34087  esumiun  34095  measssd  34216  measunl  34217  omssubadd  34302  carsgclctunlem3  34322  pmeasmono  34326  sibfof  34342  oddpwdc  34356  eulerpartlemgc  34364  iwrdsplit  34389  ballotlemsgt1  34513  ballotlemsel1i  34515  sgnmul  34545  signsply0  34566  signstfvc  34589  signsvtp  34598  signsvfpn  34600  fdvposlt  34614  fdvneggt  34615  fdvnegge  34617  logdivsqrle  34665  hgt750lemf  34668  tgoldbachgtde  34675  swrdwlk  35132  subfaclim  35193  erdszelem7  35202  erdszelem8  35203  cvmliftlem2  35291  snmlff  35334  sinccvglem  35677  climlec3  35734  faclim  35746  fnejoin1  36369  poimirlem12  37639  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem23  37650  poimirlem28  37655  broucube  37661  mblfinlem2  37665  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  itg2addnclem  37678  itg2addnclem3  37680  itg2gt0cn  37682  itggt0cn  37697  ftc1anclem5  37704  ftc1anclem7  37706  ftc1anclem8  37707  isbnd3  37791  ssbnd  37795  heiborlem8  37825  bfplem2  37830  rrncmslem  37839  rrnequiv  37842  rrntotbnd  37843  lcv1  39042  lsatcv0eq  39048  lsatcvat3  39053  cvlsupr2  39344  hlatlej2  39377  cvrval4N  39416  cvratlem  39423  atcvr0eq  39428  2atlt  39441  atbtwnex  39450  athgt  39458  1cvrat  39478  ps-1  39479  hlatexch3N  39482  hlatexch4  39483  3atlem2  39486  atcvrlln2  39521  lplnexllnN  39566  4atlem3a  39599  4atlem10b  39607  4atlem11b  39610  4atlem12b  39613  2lplnja  39621  dalemply  39656  dalemsly  39657  dalem1  39661  dalem6  39670  dalem7  39671  dalem-cly  39673  dalem11  39676  dalem12  39677  dalem16  39681  dalem17  39682  dalem38  39712  dalem44  39718  dalem61  39735  lnatexN  39781  lncvrat  39784  lncmp  39785  paddasslem2  39823  dalawlem3  39875  dalawlem6  39878  dalawlem11  39883  lhpmcvr  40025  lhp2atne  40036  lhp2at0ne  40038  lautj  40095  trlval4  40190  cdlemc2  40194  cdlemc5  40197  cdleme3b  40231  cdleme11c  40263  cdleme19a  40305  cdleme20j  40320  cdleme22f  40348  cdleme23c  40353  cdleme26f2ALTN  40366  cdleme26f2  40367  cdleme35fnpq  40451  cdleme48bw  40504  cdlemg10a  40642  cdlemg11b  40644  cdlemg17g  40669  cdlemg18c  40682  cdlemi1  40820  cdlemk52  40956  dia2dimlem1  41066  dihord1  41220  dihjatcclem4  41423  lcmineqlem15  42044  lcmineqlem19  42048  lcmineqlem22  42051  aks4d1lem1  42063  aks4d1p1p4  42072  aks4d1p1p5  42076  aks4d1p2  42078  aks4d1p3  42079  aks4d1p6  42082  aks4d1p7d1  42083  aks4d1p7  42084  aks4d1p8  42088  aks4d1p9  42089  aks6d1c1p6  42115  aks6d1c1  42117  aks6d1c2  42131  sticksstones7  42153  aks6d1c7lem1  42181  unitscyglem4  42199  metakunt7  42212  metakunt15  42220  metakunt16  42221  2xp3dxp2ge1d  42242  dvdsexpnn0  42369  prjspner01  42635  flt4lem5  42660  fltnltalem  42672  fltnlta  42673  3cubeslem1  42695  eldioph2lem1  42771  lzenom  42781  irrapxlem1  42833  irrapxlem4  42836  irrapxlem5  42837  pell14qrgt0  42870  pell1qrge1  42881  pell1qrgap  42885  pellfundge  42893  pellfundex  42897  pellfund14  42909  rmspecsqrtnq  42917  rmxypos  42959  ltrmynn0  42960  ltrmxnn0  42961  jm2.24nn  42971  jm2.17b  42973  jm2.17c  42974  jm2.24  42975  congadd  42978  congsym  42980  congneg  42981  congid  42983  mzpcong  42984  acongrep  42992  acongeq  42995  jm2.18  43000  jm2.19  43005  jm2.23  43008  jm2.25  43011  jm2.26lem3  43013  jm2.15nn0  43015  jm2.16nn0  43016  jm2.27a  43017  jm2.27c  43019  jm3.1lem1  43029  idomsubgmo  43205  sqrtcval  43654  inductionexd  44168  imo72b2lem0  44178  imo72b2  44185  dvgrat  44331  radcnvrat  44333  binomcxplemnn0  44368  binomcxplemnotnn0  44375  cncmpmax  45037  rnmptlb  45250  zltlesub  45297  infxrpnf  45457  xrpnf  45496  fmul01  45595  fmul01lt1lem1  45599  climdivf  45627  sumnnodd  45645  climinf2lem  45721  limsup10exlem  45787  climliminf  45821  dfxlim2v  45862  xlimliminflimsup  45877  dvdivbd  45938  volge0  45976  stoweidlem1  46016  stoweidlem16  46031  stoweidlem18  46033  stoweidlem24  46039  stoweidlem26  46041  stoweidlem36  46051  stoweidlem38  46053  stoweidlem41  46056  stoweidlem42  46057  stoweidlem44  46059  stoweidlem45  46060  stoweidlem48  46063  stoweidlem62  46077  wallispilem5  46084  stirlinglem1  46089  stirlinglem5  46093  stirlinglem7  46095  stirlinglem8  46096  stirlinglem9  46097  stirlinglem11  46099  fourierdlem4  46126  fourierdlem10  46132  fourierdlem37  46159  fourierdlem47  46168  fourierdlem72  46193  fourierdlem74  46195  fourierdlem79  46200  fourierdlem82  46203  fourierdlem89  46210  fourierdlem91  46212  fourierdlem93  46214  fourierdlem103  46224  fourierdlem104  46225  fourierdlem112  46233  etransclem24  46273  etransclem25  46274  etransclem28  46277  etransclem37  46286  etransclem38  46287  etransclem44  46293  meaiuninc3v  46499  vonicclem1  46698  pimconstlt0  46716  smfsuplem1  46826  rlimdmafv  47189  rlimdmafv2  47270  2elfz2melfz  47330  iccpartgtprec  47407  iccpartlt  47411  iccpartgtl  47413  sqrtpwpw2p  47525  fmtnodvds  47531  goldbachthlem1  47532  lighneallem4a  47595  perfectALTVlem1  47708  uhgrimgrlim  47954  cznnring  48178  altgsumbcALT  48269  expnegico01  48435  flnn0div2ge  48454  rege1logbrege0  48479  fllogbd  48481  nnpw2blen  48501  nnolog2flm1  48511  dignn0ldlem  48523  dignn0flhalflem1  48536  dignn0flhalflem2  48537  eenglngeehlnmlem2  48659  itsclc0yqsol  48685  2itscp  48702  itscnhlinecirc02plem1  48703  itscnhlinecirc02plem2  48704  inlinecirc02p  48708