Theorem breqtrrd 5194

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 2746	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	breqtrd 5192	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1537   class class class wbr 5166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167

This theorem is referenced by:  marypha1lem  9502  marypha2  9508  infsupprpr  9573  unxpwdom  9658  ttrcltr  9785  onadju  10263  nnadju  10267  cfss  10334  tskuni  10852  ltexnq  11044  lt2addmuld  12543  div4p1lem1div2  12548  mul2lt0rgt0  13160  prodge0ld  13165  xrmax1  13237  xrmax2  13238  max1ALT  13248  qbtwnxr  13262  xleadd1a  13315  xlt2add  13322  xlesubadd  13325  xmulgt0  13345  xlemul1a  13350  xov1plusxeqvd  13558  uzsubsubfz  13606  fzctr  13697  subfzo0  13839  flflp1  13858  fldiv4lem1div2uz2  13887  ceilge  13896  modge0  13930  modlt  13931  modid  13947  m1modge3gt1  13969  modaddmodup  13985  sermono  14085  seqf1olem1  14092  seqf1olem2  14093  sqgt0  14176  sqge0  14186  leexp1a  14225  nnlesq  14254  expnbnd  14281  expmulnbnd  14284  discr1  14288  facwordi  14338  faclbnd5  14347  nfile  14408  hashdom  14428  hashgt23el  14473  fi1uzind  14556  brfi1indALT  14559  ccatws1n0  14680  swrds2  14989  cjmulge0  15195  resqrtcl  15302  absge0  15336  sqreulem  15408  amgm2  15418  rlimdm  15597  rlimge0  15627  reccn2  15643  climle  15686  climserle  15711  isercoll2  15717  iseraltlem1  15730  iseralt  15733  isumclim2  15806  isumclim3  15807  isumge0  15814  fsumless  15844  cvgcmp  15864  cvgcmpce  15866  abscvgcvg  15867  isumsup2  15894  isumltss  15896  climcndslem1  15897  climcnds  15899  supcvg  15904  harmonic  15907  expcnv  15912  explecnv  15913  cvgrat  15931  mertenslem1  15932  mertenslem2  15933  clim2div  15937  ntrivcvgtail  15948  iprodclim2  16047  iprodclim3  16048  efcvg  16133  ege2le3  16138  efaddlem  16141  eftlub  16157  effsumlt  16159  tanhlt1  16208  ef01bndlem  16232  sin02gt0  16240  rpnnen2lem4  16265  ruclem2  16280  ruclem3  16281  ruclem9  16286  iddvdsexp  16328  dvdsadd  16350  dvdsfac  16374  dvdsexp2im  16375  dvdsmod  16377  3dvds  16379  omoe  16412  sumeven  16435  divalglem1  16442  flodddiv4t2lthalf  16464  bitsfzo  16481  bitsmod  16482  bitscmp  16484  bitsinv1lem  16487  sadcaddlem  16503  sadadd3  16507  sadaddlem  16512  dvdssqim  16601  dvdsexpim  16602  dvdsmulgcd  16603  nn0seqcvgd  16617  dvdslcm  16645  lcmgcdlem  16653  dvdslcmf  16678  lcmfunsnlem2lem2  16686  mulgcddvds  16702  qredeq  16704  cncongr2  16715  sqnprm  16749  isprm6  16761  dvdszzq  16768  prmdvdsbc  16773  nonsq  16806  hashdvds  16822  prmdiv  16832  odzdvds  16842  pythagtriplem4  16866  pcpre1  16889  pcdvdsb  16916  pcz  16928  pcprmpw2  16929  pcaddlem  16935  pcadd  16936  pcadd2  16937  pcmpt  16939  pcmptdvds  16941  fldivp1  16944  pcfaclem  16945  pockthlem  16952  prmreclem1  16963  prmreclem3  16965  prmreclem5  16967  prmreclem6  16968  4sqlem6  16990  4sqlem8  16992  4sqlem11  17002  4sqlem12  17003  4sqlem14  17005  4sqlem16  17007  vdwlem3  17030  vdwlem9  17036  vdwlem10  17037  vdwlem12  17039  ramub1lem2  17074  prmgap  17106  prmgaplcm  17107  prmgapprmo  17109  mreexexd  17706  invfuc  18044  ple1  18500  eqgen  19221  lagsubg  19235  pgpfi  19647  sylow2alem2  19660  sylow2a  19661  sylow3lem4  19672  efgsrel  19776  odadd1  19890  odadd2  19891  gexex  19895  lt6abl  19937  dprd2d2  20088  dmdprdpr  20093  ablfacrp2  20111  ablfac1c  20115  pgpfaclem1  20125  ablfac2  20133  fincygsubgodd  20156  dvdsrmul1  20395  unitmulclb  20407  subrguss  20615  rhmsubcrngc  20690  abvres  20854  znfld  21602  znunit  21605  frlmisfrlm  21891  ply1coefsupp  22322  evl1gsumadd  22383  matgsum  22464  pm2mpcl  22824  psmetxrge0  24344  isxmet2d  24358  mettri  24383  xmettri3  24384  mettri3  24385  xmetrtri2  24387  prdsxmetlem  24399  imasdsf1olem  24404  xblss2ps  24432  blss2ps  24434  blss2  24435  blssps  24455  blss  24456  prdsbl  24525  dscmet  24606  nmge0  24651  nmmtri  24656  tngngp3  24698  nlmvscnlem2  24727  nrginvrcnlem  24733  nmoix  24771  nmoleub  24773  blcvx  24839  xrsxmet  24850  opnreen  24872  xrge0tsms  24875  icopnfcnv  24992  xrhmeo  24996  lebnumii  25017  pcophtb  25081  pi1grplem  25101  nmoleub2lem  25166  ipcau2  25287  tcphcphlem1  25288  ipcau  25291  ipcnlem2  25297  rrxcph  25445  minveclem2  25479  minveclem3b  25481  pjthlem1  25490  pjthlem2  25491  ivthlem3  25507  ivth2  25509  ovolfsf  25525  ovolsslem  25538  ovollb2lem  25542  ovollb2  25543  ovolctb  25544  ovolfiniun  25555  ovolicc1  25570  ovolicc2lem4  25574  ovolicc2  25576  nulmbl2  25590  unmbl  25591  ioombl1lem4  25615  uniioombllem4  25640  uniioombllem6  25642  volivth  25661  vitalilem4  25665  itg1ge0  25740  itg1ge0a  25766  itg1lea  25767  itg1climres  25769  mbfi1fseqlem5  25774  itg2ub  25788  itg2seq  25797  itg2uba  25798  itg2splitlem  25803  itg2split  25804  itg2monolem3  25807  itg2mono  25808  itg2i1fseq2  25811  itg2addlem  25813  iblss  25860  itggt0  25899  dvferm2lem  26044  dvlip  26052  dvivthlem1  26067  dvfsumlem2  26087  dvfsumlem2OLD  26088  dvfsumlem3  26089  ftc1lem4  26100  ply1divmo  26195  ply1remlem  26224  fta1glem2  26228  idomrootle  26232  ig1pdvds  26239  plyeq0lem  26269  plydiveu  26358  fta1lem  26367  vieta1lem2  26371  aaliou3lem2  26403  aaliou3lem8  26405  ulmcn  26460  mtest  26465  itgulm  26469  radcnvlem1  26474  radcnvlt1  26479  dvradcnv  26482  pserdvlem2  26490  abelthlem2  26494  abelthlem6  26498  abelthlem7  26500  abelthlem9  26502  tangtx  26565  sinq12gt0  26567  sineq0  26584  cosordlem  26590  tanord  26598  tanregt0  26599  logrnaddcl  26634  logcj  26666  argregt0  26670  argrege0  26671  argimgt0  26672  argimlt0  26673  logimul  26674  logneg2  26675  logdivlti  26680  divlogrlim  26695  logcnlem3  26704  logcnlem4  26705  dvlog2lem  26712  logtayl  26720  rpcxpcl  26736  cxpsqrtlem  26762  cxpaddle  26813  isosctrlem1  26879  asinlem3a  26931  asinlem3  26932  asinneg  26947  asinsinlem  26952  asinsin  26953  atanlogaddlem  26974  atanlogadd  26975  atanlogsublem  26976  atanlogsub  26977  atantan  26984  atanbndlem  26986  atantayl  26998  leibpi  27003  birthdaylem3  27014  areaf  27022  cxploglim  27039  jensenlem2  27049  jensen  27050  logdiflbnd  27056  harmonicbnd4  27072  fsumharmonic  27073  zetacvg  27076  lgamgulmlem2  27091  lgamgulmlem3  27092  lgamcvg2  27116  wilthlem2  27130  wilthimp  27133  ftalem1  27134  ftalem2  27135  ftalem5  27138  basellem6  27147  basellem8  27149  basellem9  27150  chtge0  27173  chtublem  27273  logexprlim  27287  perfectlem1  27291  bcmax  27340  bposlem1  27346  bposlem2  27347  bposlem6  27351  bposlem7  27352  lgsdilem2  27395  lgsqrlem4  27411  lgsquadlem1  27442  2lgsoddprmlem2  27471  2sqlem3  27482  2sqlem8  27488  2sqblem  27493  2sqmod  27498  chebbnd1lem2  27532  chtppilimlem1  27535  chtppilim  27537  chto1ub  27538  vmadivsum  27544  rplogsumlem1  27546  rplogsumlem2  27547  dchrisum0lem1a  27548  rpvmasumlem  27549  dchrisumlem1  27551  dchrisumlem2  27552  dchrvmasumlem2  27560  dchrisum0flblem1  27570  dchrisum0flblem2  27571  dchrisum0lem1b  27577  dchrisum0lem1  27578  dchrisum0lem2a  27579  dchrisum0lem3  27581  dchrisum0  27582  mudivsum  27592  mulogsumlem  27593  mulog2sumlem1  27596  mulog2sumlem2  27597  2vmadivsumlem  27602  chpdifbndlem1  27615  selberg3lem1  27619  selberg4lem1  27622  pntrlog2bndlem1  27639  pntrlog2bndlem2  27640  pntrlog2bndlem3  27641  pntrlog2bndlem4  27642  pntpbnd1a  27647  pntpbnd1  27648  pntpbnd2  27649  pntibndlem2  27653  pntibndlem3  27654  pntlemd  27656  pntlemc  27657  pntlemb  27659  pntlemg  27660  pntlemh  27661  pntlemr  27664  pntlemf  27667  pntlemo  27669  abvcxp  27677  ostth2lem1  27680  padicabv  27692  ostth2lem2  27696  ostth2lem3  27697  ostth2lem4  27698  ostth2  27699  ostth3  27700  nodense  27755  nogt01o  27759  nosupbnd2lem1  27778  noetasuplem3  27798  maxs1  27828  maxs2  27829  cofcutr  27976  cofcutrtime  27979  addsuniflem  28052  negsunif  28105  ssltmul2  28192  precsexlem11  28259  abssge0  28287  sleabs  28290  om2noseqlt  28323  expsgt0  28433  halfcut  28434  addhalfcut  28437  tgcgr4  28557  legso  28625  krippenlem  28716  midex  28763  oppperpex  28779  ttgcontlem1  28917  axpaschlem  28973  axcontlem8  29004  upgrex  29127  nbfusgrlevtxm1  29412  finsumvtxdgeven  29588  wwlksnextproplem3  29944  clwlkclwwlk2  30035  clwlkclwwlkfolem  30039  clwwlkndivn  30112  ex-ind-dvds  30493  nvabs  30704  nmooge0  30799  nmoolb  30803  siii  30885  minvecolem2  30907  minvecolem4  30912  minvecolem5  30913  hlipgt0  30946  normge0  31158  normpyc  31178  pjhthlem1  31423  pjige0i  31722  nmoplb  31939  nmfnlb  31956  branmfn  32137  pjssdif2i  32206  stlei  32272  xlt2addrd  32765  eliccelico  32782  elicoelioo  32783  bcm1n  32800  fsumiunle  32833  ccatdmss  32916  pfxlsw2ccat  32917  wrdt2ind  32920  chnub  32984  xrge0tsmsd  33041  omndmul2  33062  psgnfzto1stlem  33093  cycpmco2lem4  33122  cycpmco2lem5  33123  cyc3conja  33150  archirngz  33169  archiabllem2c  33175  ofldchr  33309  rprmasso2  33519  rprmirred  33524  1arithufdlem3  33539  fedgmullem2  33643  extdggt0  33670  evls1fldgencl  33680  algextdeglem8  33715  rtelextdg2lem  33717  madjusmdetlem2  33774  locfinreflem  33786  xrge0iifiso  33881  nexple  33973  gsumesum  34023  esumcst  34027  esumpcvgval  34042  esumcvg  34050  esumiun  34058  measssd  34179  measunl  34180  omssubadd  34265  carsgclctunlem3  34285  pmeasmono  34289  sibfof  34305  oddpwdc  34319  eulerpartlemgc  34327  iwrdsplit  34352  ballotlemsgt1  34475  ballotlemsel1i  34477  sgnmul  34507  signsply0  34528  signstfvc  34551  signsvtp  34560  signsvfpn  34562  fdvposlt  34576  fdvneggt  34577  fdvnegge  34579  logdivsqrle  34627  hgt750lemf  34630  tgoldbachgtde  34637  swrdwlk  35094  subfaclim  35156  erdszelem7  35165  erdszelem8  35166  cvmliftlem2  35254  snmlff  35297  sinccvglem  35640  climlec3  35696  faclim  35708  fnejoin1  36334  poimirlem12  37592  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem23  37603  poimirlem28  37608  broucube  37614  mblfinlem2  37618  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  itg2addnclem  37631  itg2addnclem3  37633  itg2gt0cn  37635  itggt0cn  37650  ftc1anclem5  37657  ftc1anclem7  37659  ftc1anclem8  37660  isbnd3  37744  ssbnd  37748  heiborlem8  37778  bfplem2  37783  rrncmslem  37792  rrnequiv  37795  rrntotbnd  37796  lcv1  38997  lsatcv0eq  39003  lsatcvat3  39008  cvlsupr2  39299  hlatlej2  39332  cvrval4N  39371  cvratlem  39378  atcvr0eq  39383  2atlt  39396  atbtwnex  39405  athgt  39413  1cvrat  39433  ps-1  39434  hlatexch3N  39437  hlatexch4  39438  3atlem2  39441  atcvrlln2  39476  lplnexllnN  39521  4atlem3a  39554  4atlem10b  39562  4atlem11b  39565  4atlem12b  39568  2lplnja  39576  dalemply  39611  dalemsly  39612  dalem1  39616  dalem6  39625  dalem7  39626  dalem-cly  39628  dalem11  39631  dalem12  39632  dalem16  39636  dalem17  39637  dalem38  39667  dalem44  39673  dalem61  39690  lnatexN  39736  lncvrat  39739  lncmp  39740  paddasslem2  39778  dalawlem3  39830  dalawlem6  39833  dalawlem11  39838  lhpmcvr  39980  lhp2atne  39991  lhp2at0ne  39993  lautj  40050  trlval4  40145  cdlemc2  40149  cdlemc5  40152  cdleme3b  40186  cdleme11c  40218  cdleme19a  40260  cdleme20j  40275  cdleme22f  40303  cdleme23c  40308  cdleme26f2ALTN  40321  cdleme26f2  40322  cdleme35fnpq  40406  cdleme48bw  40459  cdlemg10a  40597  cdlemg11b  40599  cdlemg17g  40624  cdlemg18c  40637  cdlemi1  40775  cdlemk52  40911  dia2dimlem1  41021  dihord1  41175  dihjatcclem4  41378  lcmineqlem15  42000  lcmineqlem19  42004  lcmineqlem22  42007  aks4d1lem1  42019  aks4d1p1p4  42028  aks4d1p1p5  42032  aks4d1p2  42034  aks4d1p3  42035  aks4d1p6  42038  aks4d1p7d1  42039  aks4d1p7  42040  aks4d1p8  42044  aks4d1p9  42045  aks6d1c1p6  42071  aks6d1c1  42073  aks6d1c2  42087  sticksstones7  42109  aks6d1c7lem1  42137  unitscyglem4  42155  metakunt7  42168  metakunt15  42176  metakunt16  42177  2xp3dxp2ge1d  42198  dvdsexpnn0  42321  prjspner01  42580  flt4lem5  42605  fltnltalem  42617  fltnlta  42618  3cubeslem1  42640  eldioph2lem1  42716  lzenom  42726  irrapxlem1  42778  irrapxlem4  42781  irrapxlem5  42782  pell14qrgt0  42815  pell1qrge1  42826  pell1qrgap  42830  pellfundge  42838  pellfundex  42842  pellfund14  42854  rmspecsqrtnq  42862  rmxypos  42904  ltrmynn0  42905  ltrmxnn0  42906  jm2.24nn  42916  jm2.17b  42918  jm2.17c  42919  jm2.24  42920  congadd  42923  congsym  42925  congneg  42926  congid  42928  mzpcong  42929  acongrep  42937  acongeq  42940  jm2.18  42945  jm2.19  42950  jm2.23  42953  jm2.25  42956  jm2.26lem3  42958  jm2.15nn0  42960  jm2.16nn0  42961  jm2.27a  42962  jm2.27c  42964  jm3.1lem1  42974  idomsubgmo  43154  sqrtcval  43603  inductionexd  44117  imo72b2  44134  dvgrat  44281  radcnvrat  44283  binomcxplemnn0  44318  binomcxplemnotnn0  44325  cncmpmax  44932  rnmptlb  45152  zltlesub  45200  infxrpnf  45361  xrpnf  45401  fmul01  45501  fmul01lt1lem1  45505  climdivf  45533  sumnnodd  45551  climinf2lem  45627  limsup10exlem  45693  climliminf  45727  dfxlim2v  45768  xlimliminflimsup  45783  dvdivbd  45844  volge0  45882  stoweidlem1  45922  stoweidlem16  45937  stoweidlem18  45939  stoweidlem24  45945  stoweidlem26  45947  stoweidlem36  45957  stoweidlem38  45959  stoweidlem41  45962  stoweidlem42  45963  stoweidlem44  45965  stoweidlem45  45966  stoweidlem48  45969  stoweidlem62  45983  wallispilem5  45990  stirlinglem1  45995  stirlinglem5  45999  stirlinglem7  46001  stirlinglem8  46002  stirlinglem9  46003  stirlinglem11  46005  fourierdlem4  46032  fourierdlem10  46038  fourierdlem37  46065  fourierdlem47  46074  fourierdlem72  46099  fourierdlem74  46101  fourierdlem79  46106  fourierdlem82  46109  fourierdlem89  46116  fourierdlem91  46118  fourierdlem93  46120  fourierdlem103  46130  fourierdlem104  46131  fourierdlem112  46139  etransclem24  46179  etransclem25  46180  etransclem28  46183  etransclem37  46192  etransclem38  46193  etransclem44  46199  meaiuninc3v  46405  vonicclem1  46604  pimconstlt0  46622  smfsuplem1  46732  rlimdmafv  47092  rlimdmafv2  47173  2elfz2melfz  47233  iccpartgtprec  47294  iccpartlt  47298  iccpartgtl  47300  sqrtpwpw2p  47412  fmtnodvds  47418  goldbachthlem1  47419  lighneallem4a  47482  perfectALTVlem1  47595  uhgrimgrlim  47811  cznnring  47985  altgsumbcALT  48078  expnegico01  48247  flnn0div2ge  48267  rege1logbrege0  48292  fllogbd  48294  nnpw2blen  48314  nnolog2flm1  48324  dignn0ldlem  48336  dignn0flhalflem1  48349  dignn0flhalflem2  48350  eenglngeehlnmlem2  48472  itsclc0yqsol  48498  2itscp  48515  itscnhlinecirc02plem1  48516  itscnhlinecirc02plem2  48517  inlinecirc02p  48521