Theorem breqtrd 5096

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

Syntax hints:   → wi 4   = wceq 1539   class class class wbr 5070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071

This theorem is referenced by:  breqtrrd  5098  breqtrid  5107  domunsn  8863  mapdom2  8884  phplem4  8895  mapfien2  9098  wemaplem2  9236  infdifsn  9345  cantnff  9362  infxpenlem  9700  infmap2  9905  ssfin4  9997  canthp1lem1  10339  nqereq  10622  ltexnq  10662  ltbtwnnq  10665  add20  11417  mullt0  11424  ltm1  11747  recgt0  11751  prodgt0  11752  ltmul1a  11754  mulge0b  11775  recp1lt1  11803  recreclt  11804  ledivp1  11807  ledivp1i  11830  ltdivp1i  11831  eluzmn  12518  ltaddrp2d  12735  mul2lt0bi  12765  prodge0rd  12766  xleadd1a  12916  xov1plusxeqvd  13159  fz01en  13213  fzonmapblen  13361  fladdz  13473  flhalf  13478  fldiv  13508  modsubdir  13588  fzen2  13617  serle  13706  ltexp2a  13812  leexp2a  13818  exple1  13822  expubnd  13823  bernneq  13872  expmulnbnd  13878  discr1  13882  discr  13883  faclbnd6  13941  hashfz  14070  hashfun  14080  seqcoll  14106  sqeqd  14805  sqrlem7  14888  sqrtge0  14897  sqrtneglem  14906  abslt  14954  absle  14955  abstri  14970  rlimge0  15218  reccn2  15234  climaddc2  15273  isercolllem1  15304  caucvgrlem  15312  summolem2a  15355  isumge0  15406  fsumle  15439  fsumlt  15440  o1fsum  15453  supcvg  15496  expcnv  15504  geolim  15510  geolim2  15511  georeclim  15512  geo2lim  15515  mertenslem1  15524  mertens  15526  prodmolem2a  15572  efcllem  15715  ef0lem  15716  efgt0  15740  eftlub  15746  eflt  15754  sinbnd  15817  cosbnd  15818  ef01bndlem  15821  sin01gt0  15827  cos01gt0  15828  sin02gt0  15829  eirrlem  15841  rpnnen2lem11  15861  rpnnen2lem12  15862  ruclem11  15877  dvdssub2  15938  dvdsadd2b  15943  dvdsexp  15965  3dvds  15968  opoe  16000  bitsfzolem  16069  bitsinv1lem  16076  bezoutlem4  16178  dvdsgcd  16180  dvdsmulgcd  16193  bezoutr1  16202  nn0seqcvgd  16203  rpmulgcd2  16289  qredeq  16290  rpdvds  16293  prmind2  16318  divdenle  16381  hashdvds  16404  phimullem  16408  eulerthlem2  16411  prmdiveq  16415  prmdivdiv  16416  pythagtriplem4  16448  pythagtriplem10  16449  pythagtriplem19  16462  iserodd  16464  pcpre1  16471  pcadd2  16519  qexpz  16530  expnprm  16531  oddprmdvds  16532  pockthlem  16534  prmreclem2  16546  prmreclem3  16547  4sqlem7  16573  4sqlem10  16576  4sqlem11  16584  4sqlem12  16585  4sqlem14  16587  4sqlem15  16588  4sqlem16  16589  0ram  16649  ffthiso  17561  latmlej12  18112  qusgrp  18726  pgpfi1  19115  sylow1lem4  19121  sylow1lem5  19122  odcau  19124  pgpfi  19125  pgpssslw  19134  sylow3lem4  19150  sylow3lem6  19152  efgsfo  19260  frgp0  19281  odadd1  19364  odadd2  19365  odadd  19366  gexexlem  19368  lt6abl  19411  gsumzsubmcl  19434  pwsgsum  19498  dprd2dlem1  19559  dprd2d2  19562  ablfacrplem  19583  ablfacrp  19584  ablfacrp2  19585  ablfac1b  19588  ablfac1eu  19591  pgpfac1lem3a  19594  ablfaclem2  19604  dvdsrid  19808  dvdsrtr  19809  dvdsrneg  19811  unitmulcl  19821  unitgrp  19824  unitnegcl  19838  isdrng2  19916  subrguss  19954  subrgunit  19957  abvsubtri  20010  fidomndrnglem  20491  gzrngunit  20576  prmirredlem  20606  znidomb  20681  frlmgsum  20889  psrbaglesupp  21037  psrbaglesuppOLD  21038  invrvald  21733  psmetsym  23371  psmettri  23372  mettri2  23402  xmetsym  23408  xmettri  23412  prdsxmetlem  23429  xblss2ps  23462  xblss2  23463  blhalf  23466  xmsge0  23524  ngptgp  23698  nrginvrcnlem  23761  nmoeq0  23806  cnmet  23841  blcvx  23867  opnreen  23900  metdcnlem  23905  metdstri  23920  metdsle  23921  metnrmlem1  23928  metnrmlem3  23930  lebnumlem1  24030  pi1inv  24121  cphnmf  24264  ipge0  24267  ipcau2  24303  tcphcphlem1  24304  csbren  24468  minveclem2  24495  minveclem3  24498  ovolssnul  24556  ovolctb  24559  ovolunnul  24569  ovoliunlem1  24571  ovoliun2  24575  ovoliunnul  24576  ioombl1lem4  24630  uniioombllem3  24654  uniioombllem4  24655  uniioombllem5  24656  uniioombl  24658  volcn  24675  vitalilem2  24678  vitalilem5  24681  itg1lea  24782  mbfi1fseqlem6  24790  mbfi1flimlem  24792  itg2eqa  24815  itg2splitlem  24818  itg2split  24819  itg2monolem1  24820  itg2cnlem2  24832  iblabsr  24899  iblmulc2  24900  bddiblnc  24911  dveflem  25048  dvef  25049  dvferm2lem  25055  dvlip  25062  c1liplem1  25065  dveq0  25069  dvlt0  25074  dvivthlem1  25077  lhop1  25083  dvfsumle  25090  dvfsumlem4  25098  dvfsumrlim3  25102  dvfsum2  25103  ftc1a  25106  ftc1lem4  25108  deg1add  25173  ply1divex  25206  ply1rem  25233  fta1glem2  25236  fta1blem  25238  ig1pdvds  25246  plyeq0lem  25276  dgrcolem2  25340  plydivlem4  25361  plyrem  25370  fta1lem  25372  aalioulem3  25399  aaliou2b  25406  aaliou3lem3  25409  aaliou3lem8  25410  ulmcn  25463  ulmdvlem1  25464  itgulm  25472  pserulm  25486  pserdvlem2  25492  abelthlem2  25496  abelthlem5  25499  abelthlem6  25500  abelthlem7  25502  abelthlem8  25503  abelthlem9  25504  sinq12gt0  25569  sinq34lt0t  25571  cosq14gt0  25572  cosq14ge0  25573  cos02pilt1  25587  efif1olem3  25605  argimgt0  25672  argimlt0  25673  logneg2  25675  logcnlem3  25704  logcnlem4  25705  logtayllem  25719  logtayl2  25722  cxpsqrtlem  25762  cxpsqrt  25763  cxpaddlelem  25809  abscxpbnd  25811  loglesqrt  25816  ang180lem2  25865  atanlogaddlem  25968  atanlogsublem  25970  atantan  25978  atans2  25986  atantayl  25992  leibpi  25997  log2tlbnd  26000  birthdaylem2  26007  birthdaylem3  26008  cxp2limlem  26030  jensenlem2  26042  jensen  26043  logdiflbnd  26049  emcllem2  26051  emcllem4  26053  harmonicbnd4  26065  fsumharmonic  26066  lgamgulmlem2  26084  lgamgulm2  26090  lgambdd  26091  lgamucov  26092  lgamcvglem  26094  lgamcvg2  26109  gamcvg  26110  wilthlem3  26124  basellem1  26135  basellem3  26137  basellem4  26138  fsumdvdsdiaglem  26237  dvdsppwf1o  26240  dvdsmulf1o  26248  chteq0  26262  chtub  26265  chpub  26273  logfacubnd  26274  logfaclbnd  26275  logexprlim  26278  perfectlem2  26283  dchrfi  26308  bclbnd  26333  bposlem1  26337  bposlem3  26339  bposlem4  26340  bposlem6  26342  lgslem1  26350  lgsqrlem2  26400  lgsqrlem4  26402  lgseisenlem2  26429  lgsquadlem1  26433  lgsquadlem2  26434  lgsquad2lem1  26437  2sqlem3  26473  2sqlem4  26474  2sqlem8  26479  2sqlem11  26482  2sqcoprm  26488  2sqmod  26489  chebbnd1lem2  26523  chebbnd1lem3  26524  chtppilimlem1  26526  chpchtlim  26532  vmadivsum  26535  vmadivsumb  26536  rpvmasumlem  26540  dchrisumlem2  26543  dchrmusum2  26547  dchrvmasumlem2  26551  dchrvmasumlem3  26552  dchrisum0flblem2  26562  dchrisum0fno1  26564  dchrisum0re  26566  dchrisum0lem1  26569  dchrisum0lem2a  26570  mudivsum  26583  mulogsumlem  26584  mulog2sumlem2  26588  vmalogdivsum2  26591  selberglem2  26599  selbergb  26602  selberg2b  26605  logdivbnd  26609  selberg3lem1  26610  selberg3lem2  26611  selberg4lem1  26613  pntrmax  26617  pntrlog2bndlem2  26631  pntrlog2bndlem3  26632  pntrlog2bndlem5  26634  pntrlog2bndlem6a  26635  pntrlog2bndlem6  26636  pntrlog2bnd  26637  pntpbnd1a  26638  pntpbnd1  26639  pntpbnd2  26640  pntibndlem1  26642  pntibndlem2  26644  pntlemb  26650  pntlemq  26654  pntlemr  26655  pntlemj  26656  pntlemk  26659  qabvle  26678  padicabvcxp  26685  ostth2lem2  26687  ostth2lem3  26688  ostth2lem4  26689  ostth3  26691  legtrid  26856  legov3  26863  krippenlem  26955  mideulem2  26999  midex  27002  opphllem5  27016  opphllem6  27017  opphl  27019  lmieu  27049  lmiisolem  27061  ttgcontlem1  27155  colinearalglem4  27180  axpaschlem  27211  axcontlem7  27241  nbfusgrlevtxm2  27648  clwlksndivn  28351  eucrct2eupth  28510  nvge0  28936  smcnlem  28960  nmoub3i  29036  nmoub2i  29037  nmlno0lem  29056  minvecolem2  29138  htthlem  29180  norm3dif2  29414  bcs2  29445  chscllem2  29901  eigposi  30099  nmopub2tALT  30172  nmfnleub2  30189  nmlnop0iALT  30258  riesz1  30328  cnlnadjlem2  30331  nmopcoadji  30364  leopsq  30392  leopmul  30397  leopnmid  30401  nmopleid  30402  opsqrlem6  30408  0leopj  30449  hstle1  30489  strlem3a  30515  mdslmd4i  30596  cvexchlem  30631  cdj1i  30696  unidifsnel  30784  unidifsnne  30785  le2halvesd  30980  xlt2addrd  30983  fsumub  31044  wrdt2ind  31127  xrge0tsmsd  31219  fzto1st1  31271  cycpmco2lem4  31298  cycpmco2lem6  31300  cyc3conja  31326  archiabllem1a  31347  archiabllem2a  31350  archiabllem2c  31351  orngsqr  31405  ornglmulle  31406  orngrmulle  31407  orng0le1  31413  fedgmullem1  31612  fedgmullem2  31613  metideq  31745  metider  31746  sqsscirc1  31760  esummono  31922  esumpad2  31924  esumle  31926  esumlef  31930  esumcst  31931  esumrnmpt2  31936  esum2d  31961  aean  32112  dya2ub  32137  dya2icoseg  32144  omssubadd  32167  inelcarsg  32178  carsgsigalem  32182  carsggect  32185  carsgclctunlem2  32186  eulerpartlemb  32235  fibp1  32268  sgnmulsgp  32417  signsplypnf  32429  signsply0  32430  fdvposlt  32479  fdvposle  32481  reprgt  32501  logdivsqrle  32530  hgt750lemb  32536  hgt750leme  32538  tgoldbachgtde  32540  subfacval3  33051  sconnpht2  33100  sconnpi1  33101  resconn  33108  snmlff  33191  sinccvglem  33530  faclimlem2  33616  ttrclss  33706  rnttrcl  33708  btwnouttr2  34251  dnibndlem5  34589  dnibndlem7  34591  dnibndlem8  34592  dnibndlem9  34593  dnibndlem10  34594  dnibnd  34598  knoppcnlem4  34603  knoppcnlem9  34608  unbdqndv2lem1  34616  unbdqndv2lem2  34617  knoppndvlem11  34629  knoppndvlem12  34630  knoppndvlem14  34632  knoppndvlem15  34633  knoppndvlem17  34635  knoppndvlem18  34636  knoppndvlem19  34637  knoppndvlem21  34639  ltflcei  35692  poimirlem9  35713  poimirlem26  35730  poimirlem27  35731  poimirlem29  35733  heicant  35739  mblfinlem2  35742  mblfinlem3  35743  mblfinlem4  35744  volsupnfl  35749  itg2addnclem  35755  itg2addnclem3  35757  iblmulc2nc  35769  ftc1cnnclem  35775  ftc1anclem6  35782  ftc1anclem7  35783  ftc1anclem8  35784  ftc2nc  35786  dvasin  35788  geomcau  35844  bfplem2  35908  rrncmslem  35917  rrnequiv  35920  lsatcvatlem  36990  islshpcv  36994  atlatmstc  37260  cvlsupr7  37289  cvrval3  37354  cvrval5  37356  cvrexchlem  37360  atcvrj1  37372  cvrat3  37383  cvrat4  37384  atbtwn  37387  1cvratex  37414  hlatexch4  37422  3atlem1  37424  3atlem2  37425  atcvrlln2  37460  atcvrlln  37461  lplnllnneN  37497  llncvrlpln2  37498  4atlem3b  37539  lplncvrlvol2  37556  dalemswapyz  37597  dalemswapyzps  37631  dalem25  37639  dalem39  37652  dalem58  37671  dalem59  37672  lneq2at  37719  lncvrat  37723  dalawlem2  37813  dalawlem3  37814  dalawlem4  37815  dalawlem6  37817  dalawlem9  37820  dalawlem11  37822  dalawlem12  37823  lhpocnle  37957  lhpmcvr3  37966  lhpmcvr5N  37968  lhpmcvr6N  37969  4atexlemunv  38007  4atexlemc  38010  4atexlemex2  38012  lautm  38035  cdlemc2  38133  cdleme5  38181  cdleme11j  38208  cdleme16b  38220  cdlemednpq  38240  cdleme19e  38248  cdleme20i  38258  cdleme22a  38281  cdleme22cN  38283  cdleme22d  38284  cdleme22e  38285  cdleme22eALTN  38286  cdleme22f  38287  cdleme23c  38292  cdleme30a  38319  cdleme35a  38389  cdleme35b  38391  cdleme42h  38423  cdlemeg46rgv  38469  cdlemg8b  38569  cdlemg12e  38588  cdlemg13a  38592  cdlemg17pq  38613  cdlemg18c  38621  cdlemg19  38625  cdlemg21  38627  cdlemg31d  38641  cdlemg33a  38647  tendoid  38714  cdlemk4  38775  cdlemki  38782  cdlemk10  38784  cdlemksv2  38788  cdlemk12  38791  cdlemk14  38795  cdlemk15  38796  cdlemk1u  38800  cdlemk5u  38802  cdlemk12u  38813  cdlemk45  38888  cdlemk48  38891  dia2dimlem1  39005  dia2dimlem2  39006  dia2dimlem3  39007  cdlemm10N  39059  cdlemn2  39136  dihjustlem  39157  dihglbcpreN  39241  dihmeetlem3N  39246  nnproddivdvdsd  39937  lcmineqlem17  39981  lcmineqlem18  39982  3lexlogpow2ineq1  39994  3lexlogpow2ineq2  39995  3lexlogpow5ineq5  39996  aks4d1p1p3  40005  aks4d1p1p2  40006  aks4d1p1p4  40007  aks4d1p1p5  40011  aks4d1p1  40012  aks4d1p3  40014  aks4d1p8  40023  sticksstones7  40036  sticksstones10  40039  sticksstones12  40042  sticksstones22  40052  2xp3dxp2ge1d  40090  factwoffsmonot  40091  zrtdvds  40267  rtprmirr  40268  dffltz  40387  fltdvdsabdvdsc  40391  fltaccoprm  40393  fltabcoprm  40395  flt4lem5elem  40404  flt4lem7  40412  fltnlta  40416  irrapxlem1  40560  pell1qrgaplem  40611  pell1qrgap  40612  monotoddzzfi  40680  jm2.24nn  40697  congtr  40703  congmul  40705  congsub  40708  fzmaxdif  40719  acongeq  40721  jm2.20nn  40735  jm2.25  40737  hbtlem4  40867  dgrsub2  40876  mpaaeu  40891  idomsubgmo  40939  iscard4  41038  sqrtcvallem4  41136  leeq2d  41657  int-sqgeq0d  41686  int-ineqmvtd  41691  cvgdvgrat  41820  radcnvrat  41821  hashnzfzclim  41829  dvconstbi  41841  binomcxplemdvbinom  41860  isosctrlem1ALT  42443  mulltgt0  42454  rnmptbd2lem  42683  oddfl  42705  2timesgt  42716  lt3addmuld  42730  lt4addmuld  42735  supxrgere  42762  supxrgelem  42766  supxrge  42767  xadd0ge2  42770  infrpge  42780  xrlexaddrp  42781  xralrple2  42783  infxr  42796  infleinflem1  42799  infleinflem2  42800  infleinf  42801  xralrple4  42802  xralrple3  42803  recnnltrp  42806  rpgtrecnn  42809  xrralrecnnge  42820  rexabslelem  42848  infrnmptle  42853  supminfxr  42894  xrpnf  42916  iccshift  42946  iooshift  42950  ressiocsup  42982  ressioosup  42983  fsumnncl  43003  fmul01  43011  fmul01lt1lem1  43015  fmul01lt1lem2  43016  mccllem  43028  climrec  43034  climexp  43036  climneg  43041  limcrecl  43060  sumnnodd  43061  lptioo2  43062  lptioo1  43063  ltmod  43069  lptre2pt  43071  0ellimcdiv  43080  limclner  43082  fnlimcnv  43098  climinf2lem  43137  limsupubuzlem  43143  limsup10exlem  43203  limsupgtlem  43208  dfxlim2v  43278  xlimliminflimsup  43293  cncficcgt0  43319  cncfioobdlem  43327  ioodvbdlimc1lem1  43362  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvdsn1add  43370  dvnxpaek  43373  dvnmul  43374  dvnprodlem1  43377  itgiccshift  43411  itgperiod  43412  sublevolico  43415  ismbl3  43417  ovolsplit  43419  ismbl4  43424  stoweidlem1  43432  stoweidlem11  43442  stoweidlem13  43444  stoweidlem26  43457  stoweidlem34  43465  stoweidlem38  43469  stoweidlem42  43473  stoweidlem51  43482  stoweidlem59  43490  stirlinglem5  43509  stirlinglem6  43510  stirlinglem7  43511  stirlinglem10  43514  stirlinglem11  43515  stirlinglem13  43517  stirlinglem15  43519  dirkercncflem1  43534  dirkercncflem4  43537  fourierdlem4  43542  fourierdlem10  43548  fourierdlem11  43549  fourierdlem15  43553  fourierdlem20  43558  fourierdlem25  43563  fourierdlem26  43564  fourierdlem30  43568  fourierdlem37  43575  fourierdlem39  43577  fourierdlem40  43578  fourierdlem41  43579  fourierdlem42  43580  fourierdlem44  43582  fourierdlem47  43584  fourierdlem48  43585  fourierdlem49  43586  fourierdlem50  43587  fourierdlem51  43588  fourierdlem52  43589  fourierdlem54  43591  fourierdlem60  43597  fourierdlem61  43598  fourierdlem63  43600  fourierdlem64  43601  fourierdlem65  43602  fourierdlem73  43610  fourierdlem74  43611  fourierdlem75  43612  fourierdlem76  43613  fourierdlem78  43615  fourierdlem79  43616  fourierdlem81  43618  fourierdlem84  43621  fourierdlem87  43624  fourierdlem92  43629  fourierdlem93  43630  fourierdlem101  43638  fourierdlem102  43639  fourierdlem103  43640  fourierdlem104  43641  fourierdlem111  43648  fourierdlem114  43651  sqwvfoura  43659  sqwvfourb  43660  fouriersw  43662  etransclem19  43684  etransclem23  43688  etransclem24  43689  etransclem25  43690  etransclem27  43692  etransclem32  43697  etransclem35  43700  etransclem48  43713  qndenserrnbllem  43725  ioorrnopnlem  43735  ioorrnopnxrlem  43737  fsumlesge0  43805  sge0cl  43809  sge0supre  43817  sge0less  43820  sge0gerp  43823  sge0ltfirp  43828  sge0le  43835  sge0ltfirpmpt  43836  sge0split  43837  sge0rpcpnf  43849  sge0ltfirpmpt2  43854  sge0isum  43855  sge0xaddlem1  43861  sge0pnffigtmpt  43868  sge0pnffsumgt  43870  sge0gtfsumgt  43871  sge0seq  43874  nnfoctbdjlem  43883  meassle  43891  meaiuninclem  43908  meaiininclem  43914  omeiunle  43945  omeiunltfirp  43947  carageniuncllem2  43950  carageniuncl  43951  omess0  43962  hoicvr  43976  ovnlerp  43990  ovnsubaddlem1  43998  hsphoidmvle2  44013  hoidmv1lelem2  44020  hoidmv1le  44022  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvlelem5  44027  ovnhoilem2  44030  ovnhoi  44031  hoidifhspdmvle  44048  hoiqssbllem2  44051  hspmbllem2  44055  hspmbllem3  44056  hspmbl  44057  vonioolem2  44109  vonicclem2  44112  smfaddlem1  44185  smflimlem2  44194  smflimlem4  44196  smfmullem1  44212  smfinflem  44237  smflimsuplem4  44243  smflimsuplem8  44247  perfectALTVlem2  45062  nnpw2blen  45814  itscnhlinecirc02plem1  46016