Theorem breqtrd 5175

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 5161	. 2 ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐴𝑅𝐶))
4	1, 3	mpbid 231	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150

This theorem is referenced by:  breqtrrd  5177  breqtrid  5186  domunsn  9127  mapdom2  9148  phplem2  9208  phplem4OLD  9220  mapfien2  9404  wemaplem2  9542  infdifsn  9652  cantnff  9669  ttrclss  9715  rnttrcl  9717  infxpenlem  10008  infmap2  10213  ssfin4  10305  canthp1lem1  10647  nqereq  10930  ltexnq  10970  ltbtwnnq  10973  add20  11726  mullt0  11733  ltm1  12056  recgt0  12060  prodgt0  12061  ltmul1a  12063  mulge0b  12084  recp1lt1  12112  recreclt  12113  ledivp1  12116  ledivp1i  12139  ltdivp1i  12140  eluzmn  12829  ltaddrp2d  13050  mul2lt0bi  13080  prodge0rd  13081  xleadd1a  13232  xov1plusxeqvd  13475  fz01en  13529  fzonmapblen  13678  fladdz  13790  flhalf  13795  fldiv  13825  modsubdir  13905  fzen2  13934  serle  14023  ltexp2a  14131  leexp2a  14137  exple1  14141  expubnd  14142  bernneq  14192  expmulnbnd  14198  discr1  14202  discr  14203  faclbnd6  14259  hashfz  14387  hashfun  14397  seqcoll  14425  sqeqd  15113  01sqrexlem7  15195  sqrtge0  15204  sqrtneglem  15213  abslt  15261  absle  15262  abstri  15277  rlimge0  15525  reccn2  15541  climaddc2  15580  isercolllem1  15611  caucvgrlem  15619  summolem2a  15661  isumge0  15712  fsumle  15745  fsumlt  15746  o1fsum  15759  supcvg  15802  expcnv  15810  geolim  15816  geolim2  15817  georeclim  15818  geo2lim  15821  mertenslem1  15830  mertens  15832  prodmolem2a  15878  efcllem  16021  ef0lem  16022  efgt0  16046  eftlub  16052  eflt  16060  sinbnd  16123  cosbnd  16124  ef01bndlem  16127  sin01gt0  16133  cos01gt0  16134  sin02gt0  16135  eirrlem  16147  rpnnen2lem11  16167  rpnnen2lem12  16168  ruclem11  16183  dvdssub2  16244  dvdsadd2b  16249  dvdsexp  16271  3dvds  16274  opoe  16306  bitsfzolem  16375  bitsinv1lem  16382  bezoutlem4  16484  dvdsgcd  16486  dvdsmulgcd  16497  bezoutr1  16506  nn0seqcvgd  16507  rpmulgcd2  16593  qredeq  16594  rpdvds  16597  prmind2  16622  divdenle  16685  hashdvds  16708  phimullem  16712  eulerthlem2  16715  prmdiveq  16719  prmdivdiv  16720  pythagtriplem4  16752  pythagtriplem10  16753  pythagtriplem19  16766  iserodd  16768  pcpre1  16775  pcadd2  16823  qexpz  16834  expnprm  16835  oddprmdvds  16836  pockthlem  16838  prmreclem2  16850  prmreclem3  16851  4sqlem7  16877  4sqlem10  16880  4sqlem11  16888  4sqlem12  16889  4sqlem14  16891  4sqlem15  16892  4sqlem16  16893  0ram  16953  ffthiso  17880  latmlej12  18432  qusgrp  19065  pgpfi1  19463  sylow1lem4  19469  sylow1lem5  19470  odcau  19472  pgpfi  19473  pgpssslw  19482  sylow3lem4  19498  sylow3lem6  19500  efgsfo  19607  frgp0  19628  odadd1  19716  odadd2  19717  odadd  19718  gexexlem  19720  lt6abl  19763  gsumzsubmcl  19786  pwsgsum  19850  dprd2dlem1  19911  dprd2d2  19914  ablfacrplem  19935  ablfacrp  19936  ablfacrp2  19937  ablfac1b  19940  ablfac1eu  19943  pgpfac1lem3a  19946  ablfaclem2  19956  dvdsrid  20181  dvdsrtr  20182  dvdsrneg  20184  unitmulcl  20194  unitgrp  20197  unitnegcl  20211  subrguss  20334  subrgunit  20337  isdrng2  20371  abvsubtri  20443  fidomndrnglem  20925  gzrngunit  21011  prmirredlem  21042  znidomb  21117  frlmgsum  21327  psrbaglesupp  21477  psrbaglesuppOLD  21478  invrvald  22178  psmetsym  23816  psmettri  23817  mettri2  23847  xmetsym  23853  xmettri  23857  prdsxmetlem  23874  xblss2ps  23907  xblss2  23908  blhalf  23911  xmsge0  23969  ngptgp  24145  nrginvrcnlem  24208  nmoeq0  24253  cnmet  24288  blcvx  24314  opnreen  24347  metdcnlem  24352  metdstri  24367  metdsle  24368  metnrmlem1  24375  metnrmlem3  24377  lebnumlem1  24477  pi1inv  24568  cphnmf  24712  ipge0  24715  ipcau2  24751  tcphcphlem1  24752  csbren  24916  minveclem2  24943  minveclem3  24946  ovolssnul  25004  ovolctb  25007  ovolunnul  25017  ovoliunlem1  25019  ovoliun2  25023  ovoliunnul  25024  ioombl1lem4  25078  uniioombllem3  25102  uniioombllem4  25103  uniioombllem5  25104  uniioombl  25106  volcn  25123  vitalilem2  25126  vitalilem5  25129  itg1lea  25230  mbfi1fseqlem6  25238  mbfi1flimlem  25240  itg2eqa  25263  itg2splitlem  25266  itg2split  25267  itg2monolem1  25268  itg2cnlem2  25280  iblabsr  25347  iblmulc2  25348  bddiblnc  25359  dveflem  25496  dvef  25497  dvferm2lem  25503  dvlip  25510  c1liplem1  25513  dveq0  25517  dvlt0  25522  dvivthlem1  25525  lhop1  25531  dvfsumle  25538  dvfsumlem4  25546  dvfsumrlim3  25550  dvfsum2  25551  ftc1a  25554  ftc1lem4  25556  deg1add  25621  ply1divex  25654  ply1rem  25681  fta1glem2  25684  fta1blem  25686  ig1pdvds  25694  plyeq0lem  25724  dgrcolem2  25788  plydivlem4  25809  plyrem  25818  fta1lem  25820  aalioulem3  25847  aaliou2b  25854  aaliou3lem3  25857  aaliou3lem8  25858  ulmcn  25911  ulmdvlem1  25912  itgulm  25920  pserulm  25934  pserdvlem2  25940  abelthlem2  25944  abelthlem5  25947  abelthlem6  25948  abelthlem7  25950  abelthlem8  25951  abelthlem9  25952  sinq12gt0  26017  sinq34lt0t  26019  cosq14gt0  26020  cosq14ge0  26021  cos02pilt1  26035  efif1olem3  26053  argimgt0  26120  argimlt0  26121  logneg2  26123  logcnlem3  26152  logcnlem4  26153  logtayllem  26167  logtayl2  26170  cxpsqrtlem  26210  cxpsqrt  26211  cxpaddlelem  26259  abscxpbnd  26261  loglesqrt  26266  ang180lem2  26315  atanlogaddlem  26418  atanlogsublem  26420  atantan  26428  atans2  26436  atantayl  26442  leibpi  26447  log2tlbnd  26450  birthdaylem2  26457  birthdaylem3  26458  cxp2limlem  26480  jensenlem2  26492  jensen  26493  logdiflbnd  26499  emcllem2  26501  emcllem4  26503  harmonicbnd4  26515  fsumharmonic  26516  lgamgulmlem2  26534  lgamgulm2  26540  lgambdd  26541  lgamucov  26542  lgamcvglem  26544  lgamcvg2  26559  gamcvg  26560  wilthlem3  26574  basellem1  26585  basellem3  26587  basellem4  26588  fsumdvdsdiaglem  26687  dvdsppwf1o  26690  dvdsmulf1o  26698  chteq0  26712  chtub  26715  chpub  26723  logfacubnd  26724  logfaclbnd  26725  logexprlim  26728  perfectlem2  26733  dchrfi  26758  bclbnd  26783  bposlem1  26787  bposlem3  26789  bposlem4  26790  bposlem6  26792  lgslem1  26800  lgsqrlem2  26850  lgsqrlem4  26852  lgseisenlem2  26879  lgsquadlem1  26883  lgsquadlem2  26884  lgsquad2lem1  26887  2sqlem3  26923  2sqlem4  26924  2sqlem8  26929  2sqlem11  26932  2sqcoprm  26938  2sqmod  26939  chebbnd1lem2  26973  chebbnd1lem3  26974  chtppilimlem1  26976  chpchtlim  26982  vmadivsum  26985  vmadivsumb  26986  rpvmasumlem  26990  dchrisumlem2  26993  dchrmusum2  26997  dchrvmasumlem2  27001  dchrvmasumlem3  27002  dchrisum0flblem2  27012  dchrisum0fno1  27014  dchrisum0re  27016  dchrisum0lem1  27019  dchrisum0lem2a  27020  mudivsum  27033  mulogsumlem  27034  mulog2sumlem2  27038  vmalogdivsum2  27041  selberglem2  27049  selbergb  27052  selberg2b  27055  logdivbnd  27059  selberg3lem1  27060  selberg3lem2  27061  selberg4lem1  27063  pntrmax  27067  pntrlog2bndlem2  27081  pntrlog2bndlem3  27082  pntrlog2bndlem5  27084  pntrlog2bndlem6a  27085  pntrlog2bndlem6  27086  pntrlog2bnd  27087  pntpbnd1a  27088  pntpbnd1  27089  pntpbnd2  27090  pntibndlem1  27092  pntibndlem2  27094  pntlemb  27100  pntlemq  27104  pntlemr  27105  pntlemj  27106  pntlemk  27109  qabvle  27128  padicabvcxp  27135  ostth2lem2  27137  ostth2lem3  27138  ostth2lem4  27139  ostth3  27141  addsuniflem  27487  negsid  27518  negsunif  27532  mulsuniflem  27607  sltmul2  27626  precsexlem9  27664  legtrid  27873  legov3  27880  krippenlem  27972  mideulem2  28016  midex  28019  opphllem5  28033  opphllem6  28034  opphl  28036  lmieu  28066  lmiisolem  28078  ttgcontlem1  28173  colinearalglem4  28198  axpaschlem  28229  axcontlem7  28259  nbfusgrlevtxm2  28666  clwlksndivn  29370  eucrct2eupth  29529  nvge0  29957  smcnlem  29981  nmoub3i  30057  nmoub2i  30058  nmlno0lem  30077  minvecolem2  30159  htthlem  30201  norm3dif2  30435  bcs2  30466  chscllem2  30922  eigposi  31120  nmopub2tALT  31193  nmfnleub2  31210  nmlnop0iALT  31279  riesz1  31349  cnlnadjlem2  31352  nmopcoadji  31385  leopsq  31413  leopmul  31418  leopnmid  31422  nmopleid  31423  opsqrlem6  31429  0leopj  31470  hstle1  31510  strlem3a  31536  mdslmd4i  31617  cvexchlem  31652  cdj1i  31717  unidifsnel  31803  unidifsnne  31804  le2halvesd  31999  xlt2addrd  32002  fsumub  32065  wrdt2ind  32148  xrge0tsmsd  32240  fzto1st1  32292  cycpmco2lem4  32319  cycpmco2lem6  32321  cyc3conja  32347  archiabllem1a  32368  archiabllem2a  32371  archiabllem2c  32372  orngsqr  32453  ornglmulle  32454  orngrmulle  32455  orng0le1  32461  fedgmullem1  32745  fedgmullem2  32746  metideq  32904  metider  32905  sqsscirc1  32919  esummono  33083  esumpad2  33085  esumle  33087  esumlef  33091  esumcst  33092  esumrnmpt2  33097  esum2d  33122  aean  33273  dya2ub  33300  dya2icoseg  33307  omssubadd  33330  inelcarsg  33341  carsgsigalem  33345  carsggect  33348  carsgclctunlem2  33349  eulerpartlemb  33398  fibp1  33431  sgnmulsgp  33580  signsplypnf  33592  signsply0  33593  fdvposlt  33642  fdvposle  33644  reprgt  33664  logdivsqrle  33693  hgt750lemb  33699  hgt750leme  33701  tgoldbachgtde  33703  subfacval3  34211  sconnpht2  34260  sconnpi1  34261  resconn  34268  snmlff  34351  sinccvglem  34688  faclimlem2  34745  btwnouttr2  35025  gg-dvfsumle  35213  dnibndlem5  35406  dnibndlem7  35408  dnibndlem8  35409  dnibndlem9  35410  dnibndlem10  35411  dnibnd  35415  knoppcnlem4  35420  knoppcnlem9  35425  unbdqndv2lem1  35433  unbdqndv2lem2  35434  knoppndvlem11  35446  knoppndvlem12  35447  knoppndvlem14  35449  knoppndvlem15  35450  knoppndvlem17  35452  knoppndvlem18  35453  knoppndvlem19  35454  knoppndvlem21  35456  ltflcei  36524  poimirlem9  36545  poimirlem26  36562  poimirlem27  36563  poimirlem29  36565  heicant  36571  mblfinlem2  36574  mblfinlem3  36575  mblfinlem4  36576  volsupnfl  36581  itg2addnclem  36587  itg2addnclem3  36589  iblmulc2nc  36601  ftc1cnnclem  36607  ftc1anclem6  36614  ftc1anclem7  36615  ftc1anclem8  36616  ftc2nc  36618  dvasin  36620  geomcau  36675  bfplem2  36739  rrncmslem  36748  rrnequiv  36751  lsatcvatlem  37967  islshpcv  37971  atlatmstc  38237  cvlsupr7  38266  cvrval3  38332  cvrval5  38334  cvrexchlem  38338  atcvrj1  38350  cvrat3  38361  cvrat4  38362  atbtwn  38365  1cvratex  38392  hlatexch4  38400  3atlem1  38402  3atlem2  38403  atcvrlln2  38438  atcvrlln  38439  lplnllnneN  38475  llncvrlpln2  38476  4atlem3b  38517  lplncvrlvol2  38534  dalemswapyz  38575  dalemswapyzps  38609  dalem25  38617  dalem39  38630  dalem58  38649  dalem59  38650  lneq2at  38697  lncvrat  38701  dalawlem2  38791  dalawlem3  38792  dalawlem4  38793  dalawlem6  38795  dalawlem9  38798  dalawlem11  38800  dalawlem12  38801  lhpocnle  38935  lhpmcvr3  38944  lhpmcvr5N  38946  lhpmcvr6N  38947  4atexlemunv  38985  4atexlemc  38988  4atexlemex2  38990  lautm  39013  cdlemc2  39111  cdleme5  39159  cdleme11j  39186  cdleme16b  39198  cdlemednpq  39218  cdleme19e  39226  cdleme20i  39236  cdleme22a  39259  cdleme22cN  39261  cdleme22d  39262  cdleme22e  39263  cdleme22eALTN  39264  cdleme22f  39265  cdleme23c  39270  cdleme30a  39297  cdleme35a  39367  cdleme35b  39369  cdleme42h  39401  cdlemeg46rgv  39447  cdlemg8b  39547  cdlemg12e  39566  cdlemg13a  39570  cdlemg17pq  39591  cdlemg18c  39599  cdlemg19  39603  cdlemg21  39605  cdlemg31d  39619  cdlemg33a  39625  tendoid  39692  cdlemk4  39753  cdlemki  39760  cdlemk10  39762  cdlemksv2  39766  cdlemk12  39769  cdlemk14  39773  cdlemk15  39774  cdlemk1u  39778  cdlemk5u  39780  cdlemk12u  39791  cdlemk45  39866  cdlemk48  39869  dia2dimlem1  39983  dia2dimlem2  39984  dia2dimlem3  39985  cdlemm10N  40037  cdlemn2  40114  dihjustlem  40135  dihglbcpreN  40219  dihmeetlem3N  40224  nnproddivdvdsd  40914  lcmineqlem17  40958  lcmineqlem18  40959  3lexlogpow2ineq1  40971  3lexlogpow2ineq2  40972  3lexlogpow5ineq5  40973  aks4d1p1p3  40982  aks4d1p1p2  40983  aks4d1p1p4  40984  aks4d1p1p5  40988  aks4d1p1  40989  aks4d1p3  40991  aks4d1p8  41000  sticksstones7  41016  sticksstones10  41019  sticksstones12  41022  sticksstones22  41032  2xp3dxp2ge1d  41070  factwoffsmonot  41071  evlselv  41207  zrtdvds  41284  rtprmirr  41285  dffltz  41424  fltdvdsabdvdsc  41428  fltaccoprm  41430  fltabcoprm  41432  flt4lem5elem  41441  flt4lem7  41449  fltnlta  41453  irrapxlem1  41608  pell1qrgaplem  41659  pell1qrgap  41660  monotoddzzfi  41729  jm2.24nn  41746  congtr  41752  congmul  41754  congsub  41757  fzmaxdif  41768  acongeq  41770  jm2.20nn  41784  jm2.25  41786  hbtlem4  41916  dgrsub2  41925  mpaaeu  41940  idomsubgmo  41988  iscard4  42332  sqrtcvallem4  42438  leeq2d  42957  int-sqgeq0d  42986  int-ineqmvtd  42991  cvgdvgrat  43120  radcnvrat  43121  hashnzfzclim  43129  dvconstbi  43141  binomcxplemdvbinom  43160  isosctrlem1ALT  43743  mulltgt0  43754  rnmptbd2lem  44000  oddfl  44035  2timesgt  44046  lt3addmuld  44059  lt4addmuld  44064  supxrgere  44091  supxrgelem  44095  supxrge  44096  xadd0ge2  44099  infrpge  44109  xrlexaddrp  44110  xralrple2  44112  infxr  44125  infleinflem1  44128  infleinflem2  44129  infleinf  44130  xralrple4  44131  xralrple3  44132  recnnltrp  44135  rpgtrecnn  44138  xrralrecnnge  44148  rexabslelem  44176  infrnmptle  44181  supminfxr  44222  xrpnf  44244  iccshift  44279  iooshift  44283  ressiocsup  44315  ressioosup  44316  fsumnncl  44336  fmul01  44344  fmul01lt1lem1  44348  fmul01lt1lem2  44349  mccllem  44361  climrec  44367  climexp  44369  climneg  44374  limcrecl  44393  sumnnodd  44394  lptioo2  44395  lptioo1  44396  ltmod  44402  lptre2pt  44404  0ellimcdiv  44413  limclner  44415  fnlimcnv  44431  climinf2lem  44470  limsupubuzlem  44476  limsup10exlem  44536  limsupgtlem  44541  dfxlim2v  44611  xlimliminflimsup  44626  cncficcgt0  44652  cncfioobdlem  44660  ioodvbdlimc1lem1  44695  ioodvbdlimc1lem2  44696  ioodvbdlimc2lem  44698  dvdsn1add  44703  dvnxpaek  44706  dvnmul  44707  dvnprodlem1  44710  itgiccshift  44744  itgperiod  44745  sublevolico  44748  ismbl3  44750  ovolsplit  44752  ismbl4  44757  stoweidlem1  44765  stoweidlem11  44775  stoweidlem13  44777  stoweidlem26  44790  stoweidlem34  44798  stoweidlem38  44802  stoweidlem42  44806  stoweidlem51  44815  stoweidlem59  44823  stirlinglem5  44842  stirlinglem6  44843  stirlinglem7  44844  stirlinglem10  44847  stirlinglem11  44848  stirlinglem13  44850  stirlinglem15  44852  dirkercncflem1  44867  dirkercncflem4  44870  fourierdlem4  44875  fourierdlem10  44881  fourierdlem11  44882  fourierdlem15  44886  fourierdlem20  44891  fourierdlem25  44896  fourierdlem26  44897  fourierdlem30  44901  fourierdlem37  44908  fourierdlem39  44910  fourierdlem40  44911  fourierdlem41  44912  fourierdlem42  44913  fourierdlem44  44915  fourierdlem47  44917  fourierdlem48  44918  fourierdlem49  44919  fourierdlem50  44920  fourierdlem51  44921  fourierdlem52  44922  fourierdlem54  44924  fourierdlem60  44930  fourierdlem61  44931  fourierdlem63  44933  fourierdlem64  44934  fourierdlem65  44935  fourierdlem73  44943  fourierdlem74  44944  fourierdlem75  44945  fourierdlem76  44946  fourierdlem78  44948  fourierdlem79  44949  fourierdlem81  44951  fourierdlem84  44954  fourierdlem87  44957  fourierdlem92  44962  fourierdlem93  44963  fourierdlem101  44971  fourierdlem102  44972  fourierdlem103  44973  fourierdlem104  44974  fourierdlem111  44981  fourierdlem114  44984  sqwvfoura  44992  sqwvfourb  44993  fouriersw  44995  etransclem19  45017  etransclem23  45021  etransclem24  45022  etransclem25  45023  etransclem27  45025  etransclem32  45030  etransclem35  45033  etransclem48  45046  qndenserrnbllem  45058  ioorrnopnlem  45068  ioorrnopnxrlem  45070  fsumlesge0  45141  sge0cl  45145  sge0supre  45153  sge0less  45156  sge0gerp  45159  sge0ltfirp  45164  sge0le  45171  sge0ltfirpmpt  45172  sge0split  45173  sge0rpcpnf  45185  sge0ltfirpmpt2  45190  sge0isum  45191  sge0xaddlem1  45197  sge0pnffigtmpt  45204  sge0pnffsumgt  45206  sge0gtfsumgt  45207  sge0seq  45210  nnfoctbdjlem  45219  meassle  45227  meaiuninclem  45244  meaiininclem  45250  omeiunle  45281  omeiunltfirp  45283  carageniuncllem2  45286  carageniuncl  45287  omess0  45298  hoicvr  45312  ovnlerp  45326  ovnsubaddlem1  45334  hsphoidmvle2  45349  hoidmv1lelem2  45356  hoidmv1le  45358  hoidmvlelem1  45359  hoidmvlelem2  45360  hoidmvlelem3  45361  hoidmvlelem5  45363  ovnhoilem2  45366  ovnhoi  45367  hoidifhspdmvle  45384  hoiqssbllem2  45387  hspmbllem2  45391  hspmbllem3  45392  hspmbl  45393  vonioolem2  45445  vonicclem2  45448  smfaddlem1  45527  smflimlem2  45536  smflimlem4  45538  smfmullem1  45555  smfinflem  45581  smflimsuplem4  45587  smflimsuplem8  45591  perfectALTVlem2  46438  nnpw2blen  47314  itscnhlinecirc02plem1  47516