Theorem breqtrd 5174

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

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

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 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149

This theorem is referenced by:  breqtrrd  5176  breqtrid  5185  domunsn  9124  mapdom2  9145  phplem2  9205  phplem4OLD  9217  mapfien2  9401  wemaplem2  9539  infdifsn  9649  cantnff  9666  ttrclss  9712  rnttrcl  9714  infxpenlem  10005  infmap2  10210  ssfin4  10302  canthp1lem1  10644  nqereq  10927  ltexnq  10967  ltbtwnnq  10970  add20  11723  mullt0  11730  ltm1  12053  recgt0  12057  prodgt0  12058  ltmul1a  12060  mulge0b  12081  recp1lt1  12109  recreclt  12110  ledivp1  12113  ledivp1i  12136  ltdivp1i  12137  eluzmn  12826  ltaddrp2d  13047  mul2lt0bi  13077  prodge0rd  13078  xleadd1a  13229  xov1plusxeqvd  13472  fz01en  13526  fzonmapblen  13675  fladdz  13787  flhalf  13792  fldiv  13822  modsubdir  13902  fzen2  13931  serle  14020  ltexp2a  14128  leexp2a  14134  exple1  14138  expubnd  14139  bernneq  14189  expmulnbnd  14195  discr1  14199  discr  14200  faclbnd6  14256  hashfz  14384  hashfun  14394  seqcoll  14422  sqeqd  15110  01sqrexlem7  15192  sqrtge0  15201  sqrtneglem  15210  abslt  15258  absle  15259  abstri  15274  rlimge0  15522  reccn2  15538  climaddc2  15577  isercolllem1  15608  caucvgrlem  15616  summolem2a  15658  isumge0  15709  fsumle  15742  fsumlt  15743  o1fsum  15756  supcvg  15799  expcnv  15807  geolim  15813  geolim2  15814  georeclim  15815  geo2lim  15818  mertenslem1  15827  mertens  15829  prodmolem2a  15875  efcllem  16018  ef0lem  16019  efgt0  16043  eftlub  16049  eflt  16057  sinbnd  16120  cosbnd  16121  ef01bndlem  16124  sin01gt0  16130  cos01gt0  16131  sin02gt0  16132  eirrlem  16144  rpnnen2lem11  16164  rpnnen2lem12  16165  ruclem11  16180  dvdssub2  16241  dvdsadd2b  16246  dvdsexp  16268  3dvds  16271  opoe  16303  bitsfzolem  16372  bitsinv1lem  16379  bezoutlem4  16481  dvdsgcd  16483  dvdsmulgcd  16494  bezoutr1  16503  nn0seqcvgd  16504  rpmulgcd2  16590  qredeq  16591  rpdvds  16594  prmind2  16619  divdenle  16682  hashdvds  16705  phimullem  16709  eulerthlem2  16712  prmdiveq  16716  prmdivdiv  16717  pythagtriplem4  16749  pythagtriplem10  16750  pythagtriplem19  16763  iserodd  16765  pcpre1  16772  pcadd2  16820  qexpz  16831  expnprm  16832  oddprmdvds  16833  pockthlem  16835  prmreclem2  16847  prmreclem3  16848  4sqlem7  16874  4sqlem10  16877  4sqlem11  16885  4sqlem12  16886  4sqlem14  16888  4sqlem15  16889  4sqlem16  16890  0ram  16950  ffthiso  17877  latmlej12  18429  qusgrp  19060  pgpfi1  19458  sylow1lem4  19464  sylow1lem5  19465  odcau  19467  pgpfi  19468  pgpssslw  19477  sylow3lem4  19493  sylow3lem6  19495  efgsfo  19602  frgp0  19623  odadd1  19711  odadd2  19712  odadd  19713  gexexlem  19715  lt6abl  19758  gsumzsubmcl  19781  pwsgsum  19845  dprd2dlem1  19906  dprd2d2  19909  ablfacrplem  19930  ablfacrp  19931  ablfacrp2  19932  ablfac1b  19935  ablfac1eu  19938  pgpfac1lem3a  19941  ablfaclem2  19951  dvdsrid  20174  dvdsrtr  20175  dvdsrneg  20177  unitmulcl  20187  unitgrp  20190  unitnegcl  20204  isdrng2  20322  subrguss  20371  subrgunit  20374  abvsubtri  20436  fidomndrnglem  20918  gzrngunit  21004  prmirredlem  21034  znidomb  21109  frlmgsum  21319  psrbaglesupp  21469  psrbaglesuppOLD  21470  invrvald  22170  psmetsym  23808  psmettri  23809  mettri2  23839  xmetsym  23845  xmettri  23849  prdsxmetlem  23866  xblss2ps  23899  xblss2  23900  blhalf  23903  xmsge0  23961  ngptgp  24137  nrginvrcnlem  24200  nmoeq0  24245  cnmet  24280  blcvx  24306  opnreen  24339  metdcnlem  24344  metdstri  24359  metdsle  24360  metnrmlem1  24367  metnrmlem3  24369  lebnumlem1  24469  pi1inv  24560  cphnmf  24704  ipge0  24707  ipcau2  24743  tcphcphlem1  24744  csbren  24908  minveclem2  24935  minveclem3  24938  ovolssnul  24996  ovolctb  24999  ovolunnul  25009  ovoliunlem1  25011  ovoliun2  25015  ovoliunnul  25016  ioombl1lem4  25070  uniioombllem3  25094  uniioombllem4  25095  uniioombllem5  25096  uniioombl  25098  volcn  25115  vitalilem2  25118  vitalilem5  25121  itg1lea  25222  mbfi1fseqlem6  25230  mbfi1flimlem  25232  itg2eqa  25255  itg2splitlem  25258  itg2split  25259  itg2monolem1  25260  itg2cnlem2  25272  iblabsr  25339  iblmulc2  25340  bddiblnc  25351  dveflem  25488  dvef  25489  dvferm2lem  25495  dvlip  25502  c1liplem1  25505  dveq0  25509  dvlt0  25514  dvivthlem1  25517  lhop1  25523  dvfsumle  25530  dvfsumlem4  25538  dvfsumrlim3  25542  dvfsum2  25543  ftc1a  25546  ftc1lem4  25548  deg1add  25613  ply1divex  25646  ply1rem  25673  fta1glem2  25676  fta1blem  25678  ig1pdvds  25686  plyeq0lem  25716  dgrcolem2  25780  plydivlem4  25801  plyrem  25810  fta1lem  25812  aalioulem3  25839  aaliou2b  25846  aaliou3lem3  25849  aaliou3lem8  25850  ulmcn  25903  ulmdvlem1  25904  itgulm  25912  pserulm  25926  pserdvlem2  25932  abelthlem2  25936  abelthlem5  25939  abelthlem6  25940  abelthlem7  25942  abelthlem8  25943  abelthlem9  25944  sinq12gt0  26009  sinq34lt0t  26011  cosq14gt0  26012  cosq14ge0  26013  cos02pilt1  26027  efif1olem3  26045  argimgt0  26112  argimlt0  26113  logneg2  26115  logcnlem3  26144  logcnlem4  26145  logtayllem  26159  logtayl2  26162  cxpsqrtlem  26202  cxpsqrt  26203  cxpaddlelem  26249  abscxpbnd  26251  loglesqrt  26256  ang180lem2  26305  atanlogaddlem  26408  atanlogsublem  26410  atantan  26418  atans2  26426  atantayl  26432  leibpi  26437  log2tlbnd  26440  birthdaylem2  26447  birthdaylem3  26448  cxp2limlem  26470  jensenlem2  26482  jensen  26483  logdiflbnd  26489  emcllem2  26491  emcllem4  26493  harmonicbnd4  26505  fsumharmonic  26506  lgamgulmlem2  26524  lgamgulm2  26530  lgambdd  26531  lgamucov  26532  lgamcvglem  26534  lgamcvg2  26549  gamcvg  26550  wilthlem3  26564  basellem1  26575  basellem3  26577  basellem4  26578  fsumdvdsdiaglem  26677  dvdsppwf1o  26680  dvdsmulf1o  26688  chteq0  26702  chtub  26705  chpub  26713  logfacubnd  26714  logfaclbnd  26715  logexprlim  26718  perfectlem2  26723  dchrfi  26748  bclbnd  26773  bposlem1  26777  bposlem3  26779  bposlem4  26780  bposlem6  26782  lgslem1  26790  lgsqrlem2  26840  lgsqrlem4  26842  lgseisenlem2  26869  lgsquadlem1  26873  lgsquadlem2  26874  lgsquad2lem1  26877  2sqlem3  26913  2sqlem4  26914  2sqlem8  26919  2sqlem11  26922  2sqcoprm  26928  2sqmod  26929  chebbnd1lem2  26963  chebbnd1lem3  26964  chtppilimlem1  26966  chpchtlim  26972  vmadivsum  26975  vmadivsumb  26976  rpvmasumlem  26980  dchrisumlem2  26983  dchrmusum2  26987  dchrvmasumlem2  26991  dchrvmasumlem3  26992  dchrisum0flblem2  27002  dchrisum0fno1  27004  dchrisum0re  27006  dchrisum0lem1  27009  dchrisum0lem2a  27010  mudivsum  27023  mulogsumlem  27024  mulog2sumlem2  27028  vmalogdivsum2  27031  selberglem2  27039  selbergb  27042  selberg2b  27045  logdivbnd  27049  selberg3lem1  27050  selberg3lem2  27051  selberg4lem1  27053  pntrmax  27057  pntrlog2bndlem2  27071  pntrlog2bndlem3  27072  pntrlog2bndlem5  27074  pntrlog2bndlem6a  27075  pntrlog2bndlem6  27076  pntrlog2bnd  27077  pntpbnd1a  27078  pntpbnd1  27079  pntpbnd2  27080  pntibndlem1  27082  pntibndlem2  27084  pntlemb  27090  pntlemq  27094  pntlemr  27095  pntlemj  27096  pntlemk  27099  qabvle  27118  padicabvcxp  27125  ostth2lem2  27127  ostth2lem3  27128  ostth2lem4  27129  ostth3  27131  addsuniflem  27474  negsid  27505  negsunif  27519  mulsuniflem  27594  sltmul2  27613  precsexlem9  27651  legtrid  27832  legov3  27839  krippenlem  27931  mideulem2  27975  midex  27978  opphllem5  27992  opphllem6  27993  opphl  27995  lmieu  28025  lmiisolem  28037  ttgcontlem1  28132  colinearalglem4  28157  axpaschlem  28188  axcontlem7  28218  nbfusgrlevtxm2  28625  clwlksndivn  29329  eucrct2eupth  29488  nvge0  29914  smcnlem  29938  nmoub3i  30014  nmoub2i  30015  nmlno0lem  30034  minvecolem2  30116  htthlem  30158  norm3dif2  30392  bcs2  30423  chscllem2  30879  eigposi  31077  nmopub2tALT  31150  nmfnleub2  31167  nmlnop0iALT  31236  riesz1  31306  cnlnadjlem2  31309  nmopcoadji  31342  leopsq  31370  leopmul  31375  leopnmid  31379  nmopleid  31380  opsqrlem6  31386  0leopj  31427  hstle1  31467  strlem3a  31493  mdslmd4i  31574  cvexchlem  31609  cdj1i  31674  unidifsnel  31760  unidifsnne  31761  le2halvesd  31956  xlt2addrd  31959  fsumub  32022  wrdt2ind  32105  xrge0tsmsd  32197  fzto1st1  32249  cycpmco2lem4  32276  cycpmco2lem6  32278  cyc3conja  32304  archiabllem1a  32325  archiabllem2a  32328  archiabllem2c  32329  orngsqr  32411  ornglmulle  32412  orngrmulle  32413  orng0le1  32419  fedgmullem1  32703  fedgmullem2  32704  metideq  32862  metider  32863  sqsscirc1  32877  esummono  33041  esumpad2  33043  esumle  33045  esumlef  33049  esumcst  33050  esumrnmpt2  33055  esum2d  33080  aean  33231  dya2ub  33258  dya2icoseg  33265  omssubadd  33288  inelcarsg  33299  carsgsigalem  33303  carsggect  33306  carsgclctunlem2  33307  eulerpartlemb  33356  fibp1  33389  sgnmulsgp  33538  signsplypnf  33550  signsply0  33551  fdvposlt  33600  fdvposle  33602  reprgt  33622  logdivsqrle  33651  hgt750lemb  33657  hgt750leme  33659  tgoldbachgtde  33661  subfacval3  34169  sconnpht2  34218  sconnpi1  34219  resconn  34226  snmlff  34309  sinccvglem  34646  faclimlem2  34703  btwnouttr2  34983  gg-dvfsumle  35171  dnibndlem5  35347  dnibndlem7  35349  dnibndlem8  35350  dnibndlem9  35351  dnibndlem10  35352  dnibnd  35356  knoppcnlem4  35361  knoppcnlem9  35366  unbdqndv2lem1  35374  unbdqndv2lem2  35375  knoppndvlem11  35387  knoppndvlem12  35388  knoppndvlem14  35390  knoppndvlem15  35391  knoppndvlem17  35393  knoppndvlem18  35394  knoppndvlem19  35395  knoppndvlem21  35397  ltflcei  36465  poimirlem9  36486  poimirlem26  36503  poimirlem27  36504  poimirlem29  36506  heicant  36512  mblfinlem2  36515  mblfinlem3  36516  mblfinlem4  36517  volsupnfl  36522  itg2addnclem  36528  itg2addnclem3  36530  iblmulc2nc  36542  ftc1cnnclem  36548  ftc1anclem6  36555  ftc1anclem7  36556  ftc1anclem8  36557  ftc2nc  36559  dvasin  36561  geomcau  36616  bfplem2  36680  rrncmslem  36689  rrnequiv  36692  lsatcvatlem  37908  islshpcv  37912  atlatmstc  38178  cvlsupr7  38207  cvrval3  38273  cvrval5  38275  cvrexchlem  38279  atcvrj1  38291  cvrat3  38302  cvrat4  38303  atbtwn  38306  1cvratex  38333  hlatexch4  38341  3atlem1  38343  3atlem2  38344  atcvrlln2  38379  atcvrlln  38380  lplnllnneN  38416  llncvrlpln2  38417  4atlem3b  38458  lplncvrlvol2  38475  dalemswapyz  38516  dalemswapyzps  38550  dalem25  38558  dalem39  38571  dalem58  38590  dalem59  38591  lneq2at  38638  lncvrat  38642  dalawlem2  38732  dalawlem3  38733  dalawlem4  38734  dalawlem6  38736  dalawlem9  38739  dalawlem11  38741  dalawlem12  38742  lhpocnle  38876  lhpmcvr3  38885  lhpmcvr5N  38887  lhpmcvr6N  38888  4atexlemunv  38926  4atexlemc  38929  4atexlemex2  38931  lautm  38954  cdlemc2  39052  cdleme5  39100  cdleme11j  39127  cdleme16b  39139  cdlemednpq  39159  cdleme19e  39167  cdleme20i  39177  cdleme22a  39200  cdleme22cN  39202  cdleme22d  39203  cdleme22e  39204  cdleme22eALTN  39205  cdleme22f  39206  cdleme23c  39211  cdleme30a  39238  cdleme35a  39308  cdleme35b  39310  cdleme42h  39342  cdlemeg46rgv  39388  cdlemg8b  39488  cdlemg12e  39507  cdlemg13a  39511  cdlemg17pq  39532  cdlemg18c  39540  cdlemg19  39544  cdlemg21  39546  cdlemg31d  39560  cdlemg33a  39566  tendoid  39633  cdlemk4  39694  cdlemki  39701  cdlemk10  39703  cdlemksv2  39707  cdlemk12  39710  cdlemk14  39714  cdlemk15  39715  cdlemk1u  39719  cdlemk5u  39721  cdlemk12u  39732  cdlemk45  39807  cdlemk48  39810  dia2dimlem1  39924  dia2dimlem2  39925  dia2dimlem3  39926  cdlemm10N  39978  cdlemn2  40055  dihjustlem  40076  dihglbcpreN  40160  dihmeetlem3N  40165  nnproddivdvdsd  40855  lcmineqlem17  40899  lcmineqlem18  40900  3lexlogpow2ineq1  40912  3lexlogpow2ineq2  40913  3lexlogpow5ineq5  40914  aks4d1p1p3  40923  aks4d1p1p2  40924  aks4d1p1p4  40925  aks4d1p1p5  40929  aks4d1p1  40930  aks4d1p3  40932  aks4d1p8  40941  sticksstones7  40957  sticksstones10  40960  sticksstones12  40963  sticksstones22  40973  2xp3dxp2ge1d  41011  factwoffsmonot  41012  evlselv  41157  zrtdvds  41233  rtprmirr  41234  dffltz  41373  fltdvdsabdvdsc  41377  fltaccoprm  41379  fltabcoprm  41381  flt4lem5elem  41390  flt4lem7  41398  fltnlta  41402  irrapxlem1  41546  pell1qrgaplem  41597  pell1qrgap  41598  monotoddzzfi  41667  jm2.24nn  41684  congtr  41690  congmul  41692  congsub  41695  fzmaxdif  41706  acongeq  41708  jm2.20nn  41722  jm2.25  41724  hbtlem4  41854  dgrsub2  41863  mpaaeu  41878  idomsubgmo  41926  iscard4  42270  sqrtcvallem4  42376  leeq2d  42895  int-sqgeq0d  42924  int-ineqmvtd  42929  cvgdvgrat  43058  radcnvrat  43059  hashnzfzclim  43067  dvconstbi  43079  binomcxplemdvbinom  43098  isosctrlem1ALT  43681  mulltgt0  43692  rnmptbd2lem  43939  oddfl  43974  2timesgt  43985  lt3addmuld  43998  lt4addmuld  44003  supxrgere  44030  supxrgelem  44034  supxrge  44035  xadd0ge2  44038  infrpge  44048  xrlexaddrp  44049  xralrple2  44051  infxr  44064  infleinflem1  44067  infleinflem2  44068  infleinf  44069  xralrple4  44070  xralrple3  44071  recnnltrp  44074  rpgtrecnn  44077  xrralrecnnge  44087  rexabslelem  44115  infrnmptle  44120  supminfxr  44161  xrpnf  44183  iccshift  44218  iooshift  44222  ressiocsup  44254  ressioosup  44255  fsumnncl  44275  fmul01  44283  fmul01lt1lem1  44287  fmul01lt1lem2  44288  mccllem  44300  climrec  44306  climexp  44308  climneg  44313  limcrecl  44332  sumnnodd  44333  lptioo2  44334  lptioo1  44335  ltmod  44341  lptre2pt  44343  0ellimcdiv  44352  limclner  44354  fnlimcnv  44370  climinf2lem  44409  limsupubuzlem  44415  limsup10exlem  44475  limsupgtlem  44480  dfxlim2v  44550  xlimliminflimsup  44565  cncficcgt0  44591  cncfioobdlem  44599  ioodvbdlimc1lem1  44634  ioodvbdlimc1lem2  44635  ioodvbdlimc2lem  44637  dvdsn1add  44642  dvnxpaek  44645  dvnmul  44646  dvnprodlem1  44649  itgiccshift  44683  itgperiod  44684  sublevolico  44687  ismbl3  44689  ovolsplit  44691  ismbl4  44696  stoweidlem1  44704  stoweidlem11  44714  stoweidlem13  44716  stoweidlem26  44729  stoweidlem34  44737  stoweidlem38  44741  stoweidlem42  44745  stoweidlem51  44754  stoweidlem59  44762  stirlinglem5  44781  stirlinglem6  44782  stirlinglem7  44783  stirlinglem10  44786  stirlinglem11  44787  stirlinglem13  44789  stirlinglem15  44791  dirkercncflem1  44806  dirkercncflem4  44809  fourierdlem4  44814  fourierdlem10  44820  fourierdlem11  44821  fourierdlem15  44825  fourierdlem20  44830  fourierdlem25  44835  fourierdlem26  44836  fourierdlem30  44840  fourierdlem37  44847  fourierdlem39  44849  fourierdlem40  44850  fourierdlem41  44851  fourierdlem42  44852  fourierdlem44  44854  fourierdlem47  44856  fourierdlem48  44857  fourierdlem49  44858  fourierdlem50  44859  fourierdlem51  44860  fourierdlem52  44861  fourierdlem54  44863  fourierdlem60  44869  fourierdlem61  44870  fourierdlem63  44872  fourierdlem64  44873  fourierdlem65  44874  fourierdlem73  44882  fourierdlem74  44883  fourierdlem75  44884  fourierdlem76  44885  fourierdlem78  44887  fourierdlem79  44888  fourierdlem81  44890  fourierdlem84  44893  fourierdlem87  44896  fourierdlem92  44901  fourierdlem93  44902  fourierdlem101  44910  fourierdlem102  44911  fourierdlem103  44912  fourierdlem104  44913  fourierdlem111  44920  fourierdlem114  44923  sqwvfoura  44931  sqwvfourb  44932  fouriersw  44934  etransclem19  44956  etransclem23  44960  etransclem24  44961  etransclem25  44962  etransclem27  44964  etransclem32  44969  etransclem35  44972  etransclem48  44985  qndenserrnbllem  44997  ioorrnopnlem  45007  ioorrnopnxrlem  45009  fsumlesge0  45080  sge0cl  45084  sge0supre  45092  sge0less  45095  sge0gerp  45098  sge0ltfirp  45103  sge0le  45110  sge0ltfirpmpt  45111  sge0split  45112  sge0rpcpnf  45124  sge0ltfirpmpt2  45129  sge0isum  45130  sge0xaddlem1  45136  sge0pnffigtmpt  45143  sge0pnffsumgt  45145  sge0gtfsumgt  45146  sge0seq  45149  nnfoctbdjlem  45158  meassle  45166  meaiuninclem  45183  meaiininclem  45189  omeiunle  45220  omeiunltfirp  45222  carageniuncllem2  45225  carageniuncl  45226  omess0  45237  hoicvr  45251  ovnlerp  45265  ovnsubaddlem1  45273  hsphoidmvle2  45288  hoidmv1lelem2  45295  hoidmv1le  45297  hoidmvlelem1  45298  hoidmvlelem2  45299  hoidmvlelem3  45300  hoidmvlelem5  45302  ovnhoilem2  45305  ovnhoi  45306  hoidifhspdmvle  45323  hoiqssbllem2  45326  hspmbllem2  45330  hspmbllem3  45331  hspmbl  45332  vonioolem2  45384  vonicclem2  45387  smfaddlem1  45466  smflimlem2  45475  smflimlem4  45477  smfmullem1  45494  smfinflem  45520  smflimsuplem4  45526  smflimsuplem8  45530  perfectALTVlem2  46377  nnpw2blen  47220  itscnhlinecirc02plem1  47422