Theorem breqtrd 5079

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

Hypotheses

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

Assertion

Ref	Expression
breqtrd	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem breqtrd

Step	Hyp	Ref	Expression
1		breqtrd.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		breqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	2	breq2d 5065	. 2 ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐴𝑅𝐶))
4	1, 3	mpbid 235	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1543   class class class wbr 5053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-br 5054

This theorem is referenced by:  breqtrrd  5081  breqtrid  5090  domunsn  8796  mapdom2  8817  phplem4  8828  mapfien2  9025  wemaplem2  9163  infdifsn  9272  cantnff  9289  infxpenlem  9627  infmap2  9832  ssfin4  9924  canthp1lem1  10266  nqereq  10549  ltexnq  10589  ltbtwnnq  10592  add20  11344  mullt0  11351  ltm1  11674  recgt0  11678  prodgt0  11679  ltmul1a  11681  mulge0b  11702  recp1lt1  11730  recreclt  11731  ledivp1  11734  ledivp1i  11757  ltdivp1i  11758  eluzmn  12445  ltaddrp2d  12662  mul2lt0bi  12692  prodge0rd  12693  xleadd1a  12843  xov1plusxeqvd  13086  fz01en  13140  fzonmapblen  13288  fladdz  13400  flhalf  13405  fldiv  13433  modsubdir  13513  fzen2  13542  serle  13631  ltexp2a  13736  leexp2a  13742  exple1  13746  expubnd  13747  bernneq  13796  expmulnbnd  13802  discr1  13806  discr  13807  faclbnd6  13865  hashfz  13994  hashfun  14004  seqcoll  14030  sqeqd  14729  sqrlem7  14812  sqrtge0  14821  sqrtneglem  14830  abslt  14878  absle  14879  abstri  14894  rlimge0  15142  reccn2  15158  climaddc2  15197  isercolllem1  15228  caucvgrlem  15236  summolem2a  15279  isumge0  15330  fsumle  15363  fsumlt  15364  o1fsum  15377  supcvg  15420  expcnv  15428  geolim  15434  geolim2  15435  georeclim  15436  geo2lim  15439  mertenslem1  15448  mertens  15450  prodmolem2a  15496  efcllem  15639  ef0lem  15640  efgt0  15664  eftlub  15670  eflt  15678  sinbnd  15741  cosbnd  15742  ef01bndlem  15745  sin01gt0  15751  cos01gt0  15752  sin02gt0  15753  eirrlem  15765  rpnnen2lem11  15785  rpnnen2lem12  15786  ruclem11  15801  dvdssub2  15862  dvdsadd2b  15867  dvdsexp  15889  3dvds  15892  opoe  15924  bitsfzolem  15993  bitsinv1lem  16000  bezoutlem4  16102  dvdsgcd  16104  dvdsmulgcd  16117  bezoutr1  16126  nn0seqcvgd  16127  rpmulgcd2  16213  qredeq  16214  rpdvds  16217  prmind2  16242  divdenle  16305  hashdvds  16328  phimullem  16332  eulerthlem2  16335  prmdiveq  16339  prmdivdiv  16340  pythagtriplem4  16372  pythagtriplem10  16373  pythagtriplem19  16386  iserodd  16388  pcpre1  16395  pcadd2  16443  qexpz  16454  expnprm  16455  oddprmdvds  16456  pockthlem  16458  prmreclem2  16470  prmreclem3  16471  4sqlem7  16497  4sqlem10  16500  4sqlem11  16508  4sqlem12  16509  4sqlem14  16511  4sqlem15  16512  4sqlem16  16513  0ram  16573  ffthiso  17436  latmlej12  17985  qusgrp  18599  pgpfi1  18984  sylow1lem4  18990  sylow1lem5  18991  odcau  18993  pgpfi  18994  pgpssslw  19003  sylow3lem4  19019  sylow3lem6  19021  efgsfo  19129  frgp0  19150  odadd1  19233  odadd2  19234  odadd  19235  gexexlem  19237  lt6abl  19280  gsumzsubmcl  19303  pwsgsum  19367  dprd2dlem1  19428  dprd2d2  19431  ablfacrplem  19452  ablfacrp  19453  ablfacrp2  19454  ablfac1b  19457  ablfac1eu  19460  pgpfac1lem3a  19463  ablfaclem2  19473  dvdsrid  19669  dvdsrtr  19670  dvdsrneg  19672  unitmulcl  19682  unitgrp  19685  unitnegcl  19699  isdrng2  19777  subrguss  19815  subrgunit  19818  abvsubtri  19871  fidomndrnglem  20344  gzrngunit  20429  prmirredlem  20459  znidomb  20526  frlmgsum  20734  psrbaglesupp  20883  psrbaglesuppOLD  20884  invrvald  21573  psmetsym  23208  psmettri  23209  mettri2  23239  xmetsym  23245  xmettri  23249  prdsxmetlem  23266  xblss2ps  23299  xblss2  23300  blhalf  23303  xmsge0  23361  ngptgp  23534  nrginvrcnlem  23589  nmoeq0  23634  cnmet  23669  blcvx  23695  opnreen  23728  metdcnlem  23733  metdstri  23748  metdsle  23749  metnrmlem1  23756  metnrmlem3  23758  lebnumlem1  23858  pi1inv  23949  cphnmf  24092  ipge0  24095  ipcau2  24131  tcphcphlem1  24132  csbren  24296  minveclem2  24323  minveclem3  24326  ovolssnul  24384  ovolctb  24387  ovolunnul  24397  ovoliunlem1  24399  ovoliun2  24403  ovoliunnul  24404  ioombl1lem4  24458  uniioombllem3  24482  uniioombllem4  24483  uniioombllem5  24484  uniioombl  24486  volcn  24503  vitalilem2  24506  vitalilem5  24509  itg1lea  24610  mbfi1fseqlem6  24618  mbfi1flimlem  24620  itg2eqa  24643  itg2splitlem  24646  itg2split  24647  itg2monolem1  24648  itg2cnlem2  24660  iblabsr  24727  iblmulc2  24728  bddiblnc  24739  dveflem  24876  dvef  24877  dvferm2lem  24883  dvlip  24890  c1liplem1  24893  dveq0  24897  dvlt0  24902  dvivthlem1  24905  lhop1  24911  dvfsumle  24918  dvfsumlem4  24926  dvfsumrlim3  24930  dvfsum2  24931  ftc1a  24934  ftc1lem4  24936  deg1add  25001  ply1divex  25034  ply1rem  25061  fta1glem2  25064  fta1blem  25066  ig1pdvds  25074  plyeq0lem  25104  dgrcolem2  25168  plydivlem4  25189  plyrem  25198  fta1lem  25200  aalioulem3  25227  aaliou2b  25234  aaliou3lem3  25237  aaliou3lem8  25238  ulmcn  25291  ulmdvlem1  25292  itgulm  25300  pserulm  25314  pserdvlem2  25320  abelthlem2  25324  abelthlem5  25327  abelthlem6  25328  abelthlem7  25330  abelthlem8  25331  abelthlem9  25332  sinq12gt0  25397  sinq34lt0t  25399  cosq14gt0  25400  cosq14ge0  25401  cos02pilt1  25415  efif1olem3  25433  argimgt0  25500  argimlt0  25501  logneg2  25503  logcnlem3  25532  logcnlem4  25533  logtayllem  25547  logtayl2  25550  cxpsqrtlem  25590  cxpsqrt  25591  cxpaddlelem  25637  abscxpbnd  25639  loglesqrt  25644  ang180lem2  25693  atanlogaddlem  25796  atanlogsublem  25798  atantan  25806  atans2  25814  atantayl  25820  leibpi  25825  log2tlbnd  25828  birthdaylem2  25835  birthdaylem3  25836  cxp2limlem  25858  jensenlem2  25870  jensen  25871  logdiflbnd  25877  emcllem2  25879  emcllem4  25881  harmonicbnd4  25893  fsumharmonic  25894  lgamgulmlem2  25912  lgamgulm2  25918  lgambdd  25919  lgamucov  25920  lgamcvglem  25922  lgamcvg2  25937  gamcvg  25938  wilthlem3  25952  basellem1  25963  basellem3  25965  basellem4  25966  fsumdvdsdiaglem  26065  dvdsppwf1o  26068  dvdsmulf1o  26076  chteq0  26090  chtub  26093  chpub  26101  logfacubnd  26102  logfaclbnd  26103  logexprlim  26106  perfectlem2  26111  dchrfi  26136  bclbnd  26161  bposlem1  26165  bposlem3  26167  bposlem4  26168  bposlem6  26170  lgslem1  26178  lgsqrlem2  26228  lgsqrlem4  26230  lgseisenlem2  26257  lgsquadlem1  26261  lgsquadlem2  26262  lgsquad2lem1  26265  2sqlem3  26301  2sqlem4  26302  2sqlem8  26307  2sqlem11  26310  2sqcoprm  26316  2sqmod  26317  chebbnd1lem2  26351  chebbnd1lem3  26352  chtppilimlem1  26354  chpchtlim  26360  vmadivsum  26363  vmadivsumb  26364  rpvmasumlem  26368  dchrisumlem2  26371  dchrmusum2  26375  dchrvmasumlem2  26379  dchrvmasumlem3  26380  dchrisum0flblem2  26390  dchrisum0fno1  26392  dchrisum0re  26394  dchrisum0lem1  26397  dchrisum0lem2a  26398  mudivsum  26411  mulogsumlem  26412  mulog2sumlem2  26416  vmalogdivsum2  26419  selberglem2  26427  selbergb  26430  selberg2b  26433  logdivbnd  26437  selberg3lem1  26438  selberg3lem2  26439  selberg4lem1  26441  pntrmax  26445  pntrlog2bndlem2  26459  pntrlog2bndlem3  26460  pntrlog2bndlem5  26462  pntrlog2bndlem6a  26463  pntrlog2bndlem6  26464  pntrlog2bnd  26465  pntpbnd1a  26466  pntpbnd1  26467  pntpbnd2  26468  pntibndlem1  26470  pntibndlem2  26472  pntlemb  26478  pntlemq  26482  pntlemr  26483  pntlemj  26484  pntlemk  26487  qabvle  26506  padicabvcxp  26513  ostth2lem2  26515  ostth2lem3  26516  ostth2lem4  26517  ostth3  26519  legtrid  26682  legov3  26689  krippenlem  26781  mideulem2  26825  midex  26828  opphllem5  26842  opphllem6  26843  opphl  26845  lmieu  26875  lmiisolem  26887  ttgcontlem1  26976  colinearalglem4  27000  axpaschlem  27031  axcontlem7  27061  nbfusgrlevtxm2  27466  clwlksndivn  28169  eucrct2eupth  28328  nvge0  28754  smcnlem  28778  nmoub3i  28854  nmoub2i  28855  nmlno0lem  28874  minvecolem2  28956  htthlem  28998  norm3dif2  29232  bcs2  29263  chscllem2  29719  eigposi  29917  nmopub2tALT  29990  nmfnleub2  30007  nmlnop0iALT  30076  riesz1  30146  cnlnadjlem2  30149  nmopcoadji  30182  leopsq  30210  leopmul  30215  leopnmid  30219  nmopleid  30220  opsqrlem6  30226  0leopj  30267  hstle1  30307  strlem3a  30333  mdslmd4i  30414  cvexchlem  30449  cdj1i  30514  unidifsnel  30602  unidifsnne  30603  le2halvesd  30798  xlt2addrd  30801  fsumub  30862  wrdt2ind  30945  xrge0tsmsd  31036  fzto1st1  31088  cycpmco2lem4  31115  cycpmco2lem6  31117  cyc3conja  31143  archiabllem1a  31164  archiabllem2a  31167  archiabllem2c  31168  orngsqr  31222  ornglmulle  31223  orngrmulle  31224  orng0le1  31230  fedgmullem1  31424  fedgmullem2  31425  metideq  31557  metider  31558  sqsscirc1  31572  esummono  31734  esumpad2  31736  esumle  31738  esumlef  31742  esumcst  31743  esumrnmpt2  31748  esum2d  31773  aean  31924  dya2ub  31949  dya2icoseg  31956  omssubadd  31979  inelcarsg  31990  carsgsigalem  31994  carsggect  31997  carsgclctunlem2  31998  eulerpartlemb  32047  fibp1  32080  sgnmulsgp  32229  signsplypnf  32241  signsply0  32242  fdvposlt  32291  fdvposle  32293  reprgt  32313  logdivsqrle  32342  hgt750lemb  32348  hgt750leme  32350  tgoldbachgtde  32352  subfacval3  32864  sconnpht2  32913  sconnpi1  32914  resconn  32921  snmlff  33004  sinccvglem  33343  faclimlem2  33428  ttrclss  33519  rnttrcl  33521  btwnouttr2  34061  dnibndlem5  34399  dnibndlem7  34401  dnibndlem8  34402  dnibndlem9  34403  dnibndlem10  34404  dnibnd  34408  knoppcnlem4  34413  knoppcnlem9  34418  unbdqndv2lem1  34426  unbdqndv2lem2  34427  knoppndvlem11  34439  knoppndvlem12  34440  knoppndvlem14  34442  knoppndvlem15  34443  knoppndvlem17  34445  knoppndvlem18  34446  knoppndvlem19  34447  knoppndvlem21  34449  ltflcei  35502  poimirlem9  35523  poimirlem26  35540  poimirlem27  35541  poimirlem29  35543  heicant  35549  mblfinlem2  35552  mblfinlem3  35553  mblfinlem4  35554  volsupnfl  35559  itg2addnclem  35565  itg2addnclem3  35567  iblmulc2nc  35579  ftc1cnnclem  35585  ftc1anclem6  35592  ftc1anclem7  35593  ftc1anclem8  35594  ftc2nc  35596  dvasin  35598  geomcau  35654  bfplem2  35718  rrncmslem  35727  rrnequiv  35730  lsatcvatlem  36800  islshpcv  36804  atlatmstc  37070  cvlsupr7  37099  cvrval3  37164  cvrval5  37166  cvrexchlem  37170  atcvrj1  37182  cvrat3  37193  cvrat4  37194  atbtwn  37197  1cvratex  37224  hlatexch4  37232  3atlem1  37234  3atlem2  37235  atcvrlln2  37270  atcvrlln  37271  lplnllnneN  37307  llncvrlpln2  37308  4atlem3b  37349  lplncvrlvol2  37366  dalemswapyz  37407  dalemswapyzps  37441  dalem25  37449  dalem39  37462  dalem58  37481  dalem59  37482  lneq2at  37529  lncvrat  37533  dalawlem2  37623  dalawlem3  37624  dalawlem4  37625  dalawlem6  37627  dalawlem9  37630  dalawlem11  37632  dalawlem12  37633  lhpocnle  37767  lhpmcvr3  37776  lhpmcvr5N  37778  lhpmcvr6N  37779  4atexlemunv  37817  4atexlemc  37820  4atexlemex2  37822  lautm  37845  cdlemc2  37943  cdleme5  37991  cdleme11j  38018  cdleme16b  38030  cdlemednpq  38050  cdleme19e  38058  cdleme20i  38068  cdleme22a  38091  cdleme22cN  38093  cdleme22d  38094  cdleme22e  38095  cdleme22eALTN  38096  cdleme22f  38097  cdleme23c  38102  cdleme30a  38129  cdleme35a  38199  cdleme35b  38201  cdleme42h  38233  cdlemeg46rgv  38279  cdlemg8b  38379  cdlemg12e  38398  cdlemg13a  38402  cdlemg17pq  38423  cdlemg18c  38431  cdlemg19  38435  cdlemg21  38437  cdlemg31d  38451  cdlemg33a  38457  tendoid  38524  cdlemk4  38585  cdlemki  38592  cdlemk10  38594  cdlemksv2  38598  cdlemk12  38601  cdlemk14  38605  cdlemk15  38606  cdlemk1u  38610  cdlemk5u  38612  cdlemk12u  38623  cdlemk45  38698  cdlemk48  38701  dia2dimlem1  38815  dia2dimlem2  38816  dia2dimlem3  38817  cdlemm10N  38869  cdlemn2  38946  dihjustlem  38967  dihglbcpreN  39051  dihmeetlem3N  39056  nnproddivdvdsd  39743  lcmineqlem17  39787  lcmineqlem18  39788  3lexlogpow2ineq1  39800  3lexlogpow2ineq2  39801  3lexlogpow5ineq5  39802  aks4d1p1p3  39810  aks4d1p1p2  39811  aks4d1p1p4  39812  aks4d1p1p5  39816  aks4d1p1  39817  aks4d1p3  39819  sticksstones7  39830  sticksstones10  39833  sticksstones12  39836  sticksstones22  39846  2xp3dxp2ge1d  39884  factwoffsmonot  39885  zrtdvds  40054  rtprmirr  40055  dffltz  40174  fltdvdsabdvdsc  40178  fltaccoprm  40180  fltabcoprm  40182  flt4lem5elem  40191  flt4lem7  40199  fltnlta  40203  irrapxlem1  40347  pell1qrgaplem  40398  pell1qrgap  40399  monotoddzzfi  40467  jm2.24nn  40484  congtr  40490  congmul  40492  congsub  40495  fzmaxdif  40506  acongeq  40508  jm2.20nn  40522  jm2.25  40524  hbtlem4  40654  dgrsub2  40663  mpaaeu  40678  idomsubgmo  40726  iscard4  40825  sqrtcvallem4  40923  leeq2d  41445  int-sqgeq0d  41475  int-ineqmvtd  41480  cvgdvgrat  41604  radcnvrat  41605  hashnzfzclim  41613  dvconstbi  41625  binomcxplemdvbinom  41644  isosctrlem1ALT  42227  mulltgt0  42238  rnmptbd2lem  42466  oddfl  42488  2timesgt  42499  lt3addmuld  42513  lt4addmuld  42518  supxrgere  42545  supxrgelem  42549  supxrge  42550  xadd0ge2  42553  infrpge  42563  xrlexaddrp  42564  xralrple2  42566  infxr  42579  infleinflem1  42582  infleinflem2  42583  infleinf  42584  xralrple4  42585  xralrple3  42586  recnnltrp  42589  rpgtrecnn  42592  xrralrecnnge  42603  rexabslelem  42631  infrnmptle  42636  supminfxr  42679  xrpnf  42701  iccshift  42731  iooshift  42735  ressiocsup  42767  ressioosup  42768  fsumnncl  42788  fmul01  42796  fmul01lt1lem1  42800  fmul01lt1lem2  42801  mccllem  42813  climrec  42819  climexp  42821  climneg  42826  limcrecl  42845  sumnnodd  42846  lptioo2  42847  lptioo1  42848  ltmod  42854  lptre2pt  42856  0ellimcdiv  42865  limclner  42867  fnlimcnv  42883  climinf2lem  42922  limsupubuzlem  42928  limsup10exlem  42988  limsupgtlem  42993  dfxlim2v  43063  xlimliminflimsup  43078  cncficcgt0  43104  cncfioobdlem  43112  ioodvbdlimc1lem1  43147  ioodvbdlimc1lem2  43148  ioodvbdlimc2lem  43150  dvdsn1add  43155  dvnxpaek  43158  dvnmul  43159  dvnprodlem1  43162  itgiccshift  43196  itgperiod  43197  sublevolico  43200  ismbl3  43202  ovolsplit  43204  ismbl4  43209  stoweidlem1  43217  stoweidlem11  43227  stoweidlem13  43229  stoweidlem26  43242  stoweidlem34  43250  stoweidlem38  43254  stoweidlem42  43258  stoweidlem51  43267  stoweidlem59  43275  stirlinglem5  43294  stirlinglem6  43295  stirlinglem7  43296  stirlinglem10  43299  stirlinglem11  43300  stirlinglem13  43302  stirlinglem15  43304  dirkercncflem1  43319  dirkercncflem4  43322  fourierdlem4  43327  fourierdlem10  43333  fourierdlem11  43334  fourierdlem15  43338  fourierdlem20  43343  fourierdlem25  43348  fourierdlem26  43349  fourierdlem30  43353  fourierdlem37  43360  fourierdlem39  43362  fourierdlem40  43363  fourierdlem41  43364  fourierdlem42  43365  fourierdlem44  43367  fourierdlem47  43369  fourierdlem48  43370  fourierdlem49  43371  fourierdlem50  43372  fourierdlem51  43373  fourierdlem52  43374  fourierdlem54  43376  fourierdlem60  43382  fourierdlem61  43383  fourierdlem63  43385  fourierdlem64  43386  fourierdlem65  43387  fourierdlem73  43395  fourierdlem74  43396  fourierdlem75  43397  fourierdlem76  43398  fourierdlem78  43400  fourierdlem79  43401  fourierdlem81  43403  fourierdlem84  43406  fourierdlem87  43409  fourierdlem92  43414  fourierdlem93  43415  fourierdlem101  43423  fourierdlem102  43424  fourierdlem103  43425  fourierdlem104  43426  fourierdlem111  43433  fourierdlem114  43436  sqwvfoura  43444  sqwvfourb  43445  fouriersw  43447  etransclem19  43469  etransclem23  43473  etransclem24  43474  etransclem25  43475  etransclem27  43477  etransclem32  43482  etransclem35  43485  etransclem48  43498  qndenserrnbllem  43510  ioorrnopnlem  43520  ioorrnopnxrlem  43522  fsumlesge0  43590  sge0cl  43594  sge0supre  43602  sge0less  43605  sge0gerp  43608  sge0ltfirp  43613  sge0le  43620  sge0ltfirpmpt  43621  sge0split  43622  sge0rpcpnf  43634  sge0ltfirpmpt2  43639  sge0isum  43640  sge0xaddlem1  43646  sge0pnffigtmpt  43653  sge0pnffsumgt  43655  sge0gtfsumgt  43656  sge0seq  43659  nnfoctbdjlem  43668  meassle  43676  meaiuninclem  43693  meaiininclem  43699  omeiunle  43730  omeiunltfirp  43732  carageniuncllem2  43735  carageniuncl  43736  omess0  43747  hoicvr  43761  ovnlerp  43775  ovnsubaddlem1  43783  hsphoidmvle2  43798  hoidmv1lelem2  43805  hoidmv1le  43807  hoidmvlelem1  43808  hoidmvlelem2  43809  hoidmvlelem3  43810  hoidmvlelem5  43812  ovnhoilem2  43815  ovnhoi  43816  hoidifhspdmvle  43833  hoiqssbllem2  43836  hspmbllem2  43840  hspmbllem3  43841  hspmbl  43842  vonioolem2  43894  vonicclem2  43897  smfaddlem1  43970  smflimlem2  43979  smflimlem4  43981  smfmullem1  43997  smfinflem  44022  smflimsuplem4  44028  smflimsuplem8  44032  perfectALTVlem2  44847  nnpw2blen  45599  itscnhlinecirc02plem1  45801