Theorem breqtrd 5101

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

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

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076

This theorem is referenced by:  breqtrrd  5103  breqtrid  5112  domunsn  8923  mapdom2  8944  phplem2  9000  phplem4OLD  9012  mapfien2  9177  wemaplem2  9315  infdifsn  9424  cantnff  9441  ttrclss  9487  rnttrcl  9489  infxpenlem  9778  infmap2  9983  ssfin4  10075  canthp1lem1  10417  nqereq  10700  ltexnq  10740  ltbtwnnq  10743  add20  11496  mullt0  11503  ltm1  11826  recgt0  11830  prodgt0  11831  ltmul1a  11833  mulge0b  11854  recp1lt1  11882  recreclt  11883  ledivp1  11886  ledivp1i  11909  ltdivp1i  11910  eluzmn  12598  ltaddrp2d  12815  mul2lt0bi  12845  prodge0rd  12846  xleadd1a  12996  xov1plusxeqvd  13239  fz01en  13293  fzonmapblen  13442  fladdz  13554  flhalf  13559  fldiv  13589  modsubdir  13669  fzen2  13698  serle  13787  ltexp2a  13893  leexp2a  13899  exple1  13903  expubnd  13904  bernneq  13953  expmulnbnd  13959  discr1  13963  discr  13964  faclbnd6  14022  hashfz  14151  hashfun  14161  seqcoll  14187  sqeqd  14886  sqrlem7  14969  sqrtge0  14978  sqrtneglem  14987  abslt  15035  absle  15036  abstri  15051  rlimge0  15299  reccn2  15315  climaddc2  15354  isercolllem1  15385  caucvgrlem  15393  summolem2a  15436  isumge0  15487  fsumle  15520  fsumlt  15521  o1fsum  15534  supcvg  15577  expcnv  15585  geolim  15591  geolim2  15592  georeclim  15593  geo2lim  15596  mertenslem1  15605  mertens  15607  prodmolem2a  15653  efcllem  15796  ef0lem  15797  efgt0  15821  eftlub  15827  eflt  15835  sinbnd  15898  cosbnd  15899  ef01bndlem  15902  sin01gt0  15908  cos01gt0  15909  sin02gt0  15910  eirrlem  15922  rpnnen2lem11  15942  rpnnen2lem12  15943  ruclem11  15958  dvdssub2  16019  dvdsadd2b  16024  dvdsexp  16046  3dvds  16049  opoe  16081  bitsfzolem  16150  bitsinv1lem  16157  bezoutlem4  16259  dvdsgcd  16261  dvdsmulgcd  16274  bezoutr1  16283  nn0seqcvgd  16284  rpmulgcd2  16370  qredeq  16371  rpdvds  16374  prmind2  16399  divdenle  16462  hashdvds  16485  phimullem  16489  eulerthlem2  16492  prmdiveq  16496  prmdivdiv  16497  pythagtriplem4  16529  pythagtriplem10  16530  pythagtriplem19  16543  iserodd  16545  pcpre1  16552  pcadd2  16600  qexpz  16611  expnprm  16612  oddprmdvds  16613  pockthlem  16615  prmreclem2  16627  prmreclem3  16628  4sqlem7  16654  4sqlem10  16657  4sqlem11  16665  4sqlem12  16666  4sqlem14  16668  4sqlem15  16669  4sqlem16  16670  0ram  16730  ffthiso  17654  latmlej12  18206  qusgrp  18820  pgpfi1  19209  sylow1lem4  19215  sylow1lem5  19216  odcau  19218  pgpfi  19219  pgpssslw  19228  sylow3lem4  19244  sylow3lem6  19246  efgsfo  19354  frgp0  19375  odadd1  19458  odadd2  19459  odadd  19460  gexexlem  19462  lt6abl  19505  gsumzsubmcl  19528  pwsgsum  19592  dprd2dlem1  19653  dprd2d2  19656  ablfacrplem  19677  ablfacrp  19678  ablfacrp2  19679  ablfac1b  19682  ablfac1eu  19685  pgpfac1lem3a  19688  ablfaclem2  19698  dvdsrid  19902  dvdsrtr  19903  dvdsrneg  19905  unitmulcl  19915  unitgrp  19918  unitnegcl  19932  isdrng2  20010  subrguss  20048  subrgunit  20051  abvsubtri  20104  fidomndrnglem  20587  gzrngunit  20673  prmirredlem  20703  znidomb  20778  frlmgsum  20988  psrbaglesupp  21136  psrbaglesuppOLD  21137  invrvald  21834  psmetsym  23472  psmettri  23473  mettri2  23503  xmetsym  23509  xmettri  23513  prdsxmetlem  23530  xblss2ps  23563  xblss2  23564  blhalf  23567  xmsge0  23625  ngptgp  23801  nrginvrcnlem  23864  nmoeq0  23909  cnmet  23944  blcvx  23970  opnreen  24003  metdcnlem  24008  metdstri  24023  metdsle  24024  metnrmlem1  24031  metnrmlem3  24033  lebnumlem1  24133  pi1inv  24224  cphnmf  24368  ipge0  24371  ipcau2  24407  tcphcphlem1  24408  csbren  24572  minveclem2  24599  minveclem3  24602  ovolssnul  24660  ovolctb  24663  ovolunnul  24673  ovoliunlem1  24675  ovoliun2  24679  ovoliunnul  24680  ioombl1lem4  24734  uniioombllem3  24758  uniioombllem4  24759  uniioombllem5  24760  uniioombl  24762  volcn  24779  vitalilem2  24782  vitalilem5  24785  itg1lea  24886  mbfi1fseqlem6  24894  mbfi1flimlem  24896  itg2eqa  24919  itg2splitlem  24922  itg2split  24923  itg2monolem1  24924  itg2cnlem2  24936  iblabsr  25003  iblmulc2  25004  bddiblnc  25015  dveflem  25152  dvef  25153  dvferm2lem  25159  dvlip  25166  c1liplem1  25169  dveq0  25173  dvlt0  25178  dvivthlem1  25181  lhop1  25187  dvfsumle  25194  dvfsumlem4  25202  dvfsumrlim3  25206  dvfsum2  25207  ftc1a  25210  ftc1lem4  25212  deg1add  25277  ply1divex  25310  ply1rem  25337  fta1glem2  25340  fta1blem  25342  ig1pdvds  25350  plyeq0lem  25380  dgrcolem2  25444  plydivlem4  25465  plyrem  25474  fta1lem  25476  aalioulem3  25503  aaliou2b  25510  aaliou3lem3  25513  aaliou3lem8  25514  ulmcn  25567  ulmdvlem1  25568  itgulm  25576  pserulm  25590  pserdvlem2  25596  abelthlem2  25600  abelthlem5  25603  abelthlem6  25604  abelthlem7  25606  abelthlem8  25607  abelthlem9  25608  sinq12gt0  25673  sinq34lt0t  25675  cosq14gt0  25676  cosq14ge0  25677  cos02pilt1  25691  efif1olem3  25709  argimgt0  25776  argimlt0  25777  logneg2  25779  logcnlem3  25808  logcnlem4  25809  logtayllem  25823  logtayl2  25826  cxpsqrtlem  25866  cxpsqrt  25867  cxpaddlelem  25913  abscxpbnd  25915  loglesqrt  25920  ang180lem2  25969  atanlogaddlem  26072  atanlogsublem  26074  atantan  26082  atans2  26090  atantayl  26096  leibpi  26101  log2tlbnd  26104  birthdaylem2  26111  birthdaylem3  26112  cxp2limlem  26134  jensenlem2  26146  jensen  26147  logdiflbnd  26153  emcllem2  26155  emcllem4  26157  harmonicbnd4  26169  fsumharmonic  26170  lgamgulmlem2  26188  lgamgulm2  26194  lgambdd  26195  lgamucov  26196  lgamcvglem  26198  lgamcvg2  26213  gamcvg  26214  wilthlem3  26228  basellem1  26239  basellem3  26241  basellem4  26242  fsumdvdsdiaglem  26341  dvdsppwf1o  26344  dvdsmulf1o  26352  chteq0  26366  chtub  26369  chpub  26377  logfacubnd  26378  logfaclbnd  26379  logexprlim  26382  perfectlem2  26387  dchrfi  26412  bclbnd  26437  bposlem1  26441  bposlem3  26443  bposlem4  26444  bposlem6  26446  lgslem1  26454  lgsqrlem2  26504  lgsqrlem4  26506  lgseisenlem2  26533  lgsquadlem1  26537  lgsquadlem2  26538  lgsquad2lem1  26541  2sqlem3  26577  2sqlem4  26578  2sqlem8  26583  2sqlem11  26586  2sqcoprm  26592  2sqmod  26593  chebbnd1lem2  26627  chebbnd1lem3  26628  chtppilimlem1  26630  chpchtlim  26636  vmadivsum  26639  vmadivsumb  26640  rpvmasumlem  26644  dchrisumlem2  26647  dchrmusum2  26651  dchrvmasumlem2  26655  dchrvmasumlem3  26656  dchrisum0flblem2  26666  dchrisum0fno1  26668  dchrisum0re  26670  dchrisum0lem1  26673  dchrisum0lem2a  26674  mudivsum  26687  mulogsumlem  26688  mulog2sumlem2  26692  vmalogdivsum2  26695  selberglem2  26703  selbergb  26706  selberg2b  26709  logdivbnd  26713  selberg3lem1  26714  selberg3lem2  26715  selberg4lem1  26717  pntrmax  26721  pntrlog2bndlem2  26735  pntrlog2bndlem3  26736  pntrlog2bndlem5  26738  pntrlog2bndlem6a  26739  pntrlog2bndlem6  26740  pntrlog2bnd  26741  pntpbnd1a  26742  pntpbnd1  26743  pntpbnd2  26744  pntibndlem1  26746  pntibndlem2  26748  pntlemb  26754  pntlemq  26758  pntlemr  26759  pntlemj  26760  pntlemk  26763  qabvle  26782  padicabvcxp  26789  ostth2lem2  26791  ostth2lem3  26792  ostth2lem4  26793  ostth3  26795  legtrid  26961  legov3  26968  krippenlem  27060  mideulem2  27104  midex  27107  opphllem5  27121  opphllem6  27122  opphl  27124  lmieu  27154  lmiisolem  27166  ttgcontlem1  27261  colinearalglem4  27286  axpaschlem  27317  axcontlem7  27347  nbfusgrlevtxm2  27754  clwlksndivn  28459  eucrct2eupth  28618  nvge0  29044  smcnlem  29068  nmoub3i  29144  nmoub2i  29145  nmlno0lem  29164  minvecolem2  29246  htthlem  29288  norm3dif2  29522  bcs2  29553  chscllem2  30009  eigposi  30207  nmopub2tALT  30280  nmfnleub2  30297  nmlnop0iALT  30366  riesz1  30436  cnlnadjlem2  30439  nmopcoadji  30472  leopsq  30500  leopmul  30505  leopnmid  30509  nmopleid  30510  opsqrlem6  30516  0leopj  30557  hstle1  30597  strlem3a  30623  mdslmd4i  30704  cvexchlem  30739  cdj1i  30804  unidifsnel  30892  unidifsnne  30893  le2halvesd  31087  xlt2addrd  31090  fsumub  31151  wrdt2ind  31234  xrge0tsmsd  31326  fzto1st1  31378  cycpmco2lem4  31405  cycpmco2lem6  31407  cyc3conja  31433  archiabllem1a  31454  archiabllem2a  31457  archiabllem2c  31458  orngsqr  31512  ornglmulle  31513  orngrmulle  31514  orng0le1  31520  fedgmullem1  31719  fedgmullem2  31720  metideq  31852  metider  31853  sqsscirc1  31867  esummono  32031  esumpad2  32033  esumle  32035  esumlef  32039  esumcst  32040  esumrnmpt2  32045  esum2d  32070  aean  32221  dya2ub  32246  dya2icoseg  32253  omssubadd  32276  inelcarsg  32287  carsgsigalem  32291  carsggect  32294  carsgclctunlem2  32295  eulerpartlemb  32344  fibp1  32377  sgnmulsgp  32526  signsplypnf  32538  signsply0  32539  fdvposlt  32588  fdvposle  32590  reprgt  32610  logdivsqrle  32639  hgt750lemb  32645  hgt750leme  32647  tgoldbachgtde  32649  subfacval3  33160  sconnpht2  33209  sconnpi1  33210  resconn  33217  snmlff  33300  sinccvglem  33639  faclimlem2  33719  btwnouttr2  34333  dnibndlem5  34671  dnibndlem7  34673  dnibndlem8  34674  dnibndlem9  34675  dnibndlem10  34676  dnibnd  34680  knoppcnlem4  34685  knoppcnlem9  34690  unbdqndv2lem1  34698  unbdqndv2lem2  34699  knoppndvlem11  34711  knoppndvlem12  34712  knoppndvlem14  34714  knoppndvlem15  34715  knoppndvlem17  34717  knoppndvlem18  34718  knoppndvlem19  34719  knoppndvlem21  34721  ltflcei  35774  poimirlem9  35795  poimirlem26  35812  poimirlem27  35813  poimirlem29  35815  heicant  35821  mblfinlem2  35824  mblfinlem3  35825  mblfinlem4  35826  volsupnfl  35831  itg2addnclem  35837  itg2addnclem3  35839  iblmulc2nc  35851  ftc1cnnclem  35857  ftc1anclem6  35864  ftc1anclem7  35865  ftc1anclem8  35866  ftc2nc  35868  dvasin  35870  geomcau  35926  bfplem2  35990  rrncmslem  35999  rrnequiv  36002  lsatcvatlem  37070  islshpcv  37074  atlatmstc  37340  cvlsupr7  37369  cvrval3  37434  cvrval5  37436  cvrexchlem  37440  atcvrj1  37452  cvrat3  37463  cvrat4  37464  atbtwn  37467  1cvratex  37494  hlatexch4  37502  3atlem1  37504  3atlem2  37505  atcvrlln2  37540  atcvrlln  37541  lplnllnneN  37577  llncvrlpln2  37578  4atlem3b  37619  lplncvrlvol2  37636  dalemswapyz  37677  dalemswapyzps  37711  dalem25  37719  dalem39  37732  dalem58  37751  dalem59  37752  lneq2at  37799  lncvrat  37803  dalawlem2  37893  dalawlem3  37894  dalawlem4  37895  dalawlem6  37897  dalawlem9  37900  dalawlem11  37902  dalawlem12  37903  lhpocnle  38037  lhpmcvr3  38046  lhpmcvr5N  38048  lhpmcvr6N  38049  4atexlemunv  38087  4atexlemc  38090  4atexlemex2  38092  lautm  38115  cdlemc2  38213  cdleme5  38261  cdleme11j  38288  cdleme16b  38300  cdlemednpq  38320  cdleme19e  38328  cdleme20i  38338  cdleme22a  38361  cdleme22cN  38363  cdleme22d  38364  cdleme22e  38365  cdleme22eALTN  38366  cdleme22f  38367  cdleme23c  38372  cdleme30a  38399  cdleme35a  38469  cdleme35b  38471  cdleme42h  38503  cdlemeg46rgv  38549  cdlemg8b  38649  cdlemg12e  38668  cdlemg13a  38672  cdlemg17pq  38693  cdlemg18c  38701  cdlemg19  38705  cdlemg21  38707  cdlemg31d  38721  cdlemg33a  38727  tendoid  38794  cdlemk4  38855  cdlemki  38862  cdlemk10  38864  cdlemksv2  38868  cdlemk12  38871  cdlemk14  38875  cdlemk15  38876  cdlemk1u  38880  cdlemk5u  38882  cdlemk12u  38893  cdlemk45  38968  cdlemk48  38971  dia2dimlem1  39085  dia2dimlem2  39086  dia2dimlem3  39087  cdlemm10N  39139  cdlemn2  39216  dihjustlem  39237  dihglbcpreN  39321  dihmeetlem3N  39326  nnproddivdvdsd  40016  lcmineqlem17  40060  lcmineqlem18  40061  3lexlogpow2ineq1  40073  3lexlogpow2ineq2  40074  3lexlogpow5ineq5  40075  aks4d1p1p3  40084  aks4d1p1p2  40085  aks4d1p1p4  40086  aks4d1p1p5  40090  aks4d1p1  40091  aks4d1p3  40093  aks4d1p8  40102  sticksstones7  40115  sticksstones10  40118  sticksstones12  40121  sticksstones22  40131  2xp3dxp2ge1d  40169  factwoffsmonot  40170  zrtdvds  40353  rtprmirr  40354  dffltz  40478  fltdvdsabdvdsc  40482  fltaccoprm  40484  fltabcoprm  40486  flt4lem5elem  40495  flt4lem7  40503  fltnlta  40507  irrapxlem1  40651  pell1qrgaplem  40702  pell1qrgap  40703  monotoddzzfi  40771  jm2.24nn  40788  congtr  40794  congmul  40796  congsub  40799  fzmaxdif  40810  acongeq  40812  jm2.20nn  40826  jm2.25  40828  hbtlem4  40958  dgrsub2  40967  mpaaeu  40982  idomsubgmo  41030  iscard4  41147  sqrtcvallem4  41254  leeq2d  41775  int-sqgeq0d  41804  int-ineqmvtd  41809  cvgdvgrat  41938  radcnvrat  41939  hashnzfzclim  41947  dvconstbi  41959  binomcxplemdvbinom  41978  isosctrlem1ALT  42561  mulltgt0  42572  rnmptbd2lem  42801  oddfl  42823  2timesgt  42834  lt3addmuld  42847  lt4addmuld  42852  supxrgere  42879  supxrgelem  42883  supxrge  42884  xadd0ge2  42887  infrpge  42897  xrlexaddrp  42898  xralrple2  42900  infxr  42913  infleinflem1  42916  infleinflem2  42917  infleinf  42918  xralrple4  42919  xralrple3  42920  recnnltrp  42923  rpgtrecnn  42926  xrralrecnnge  42937  rexabslelem  42965  infrnmptle  42970  supminfxr  43011  xrpnf  43033  iccshift  43063  iooshift  43067  ressiocsup  43099  ressioosup  43100  fsumnncl  43120  fmul01  43128  fmul01lt1lem1  43132  fmul01lt1lem2  43133  mccllem  43145  climrec  43151  climexp  43153  climneg  43158  limcrecl  43177  sumnnodd  43178  lptioo2  43179  lptioo1  43180  ltmod  43186  lptre2pt  43188  0ellimcdiv  43197  limclner  43199  fnlimcnv  43215  climinf2lem  43254  limsupubuzlem  43260  limsup10exlem  43320  limsupgtlem  43325  dfxlim2v  43395  xlimliminflimsup  43410  cncficcgt0  43436  cncfioobdlem  43444  ioodvbdlimc1lem1  43479  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  dvdsn1add  43487  dvnxpaek  43490  dvnmul  43491  dvnprodlem1  43494  itgiccshift  43528  itgperiod  43529  sublevolico  43532  ismbl3  43534  ovolsplit  43536  ismbl4  43541  stoweidlem1  43549  stoweidlem11  43559  stoweidlem13  43561  stoweidlem26  43574  stoweidlem34  43582  stoweidlem38  43586  stoweidlem42  43590  stoweidlem51  43599  stoweidlem59  43607  stirlinglem5  43626  stirlinglem6  43627  stirlinglem7  43628  stirlinglem10  43631  stirlinglem11  43632  stirlinglem13  43634  stirlinglem15  43636  dirkercncflem1  43651  dirkercncflem4  43654  fourierdlem4  43659  fourierdlem10  43665  fourierdlem11  43666  fourierdlem15  43670  fourierdlem20  43675  fourierdlem25  43680  fourierdlem26  43681  fourierdlem30  43685  fourierdlem37  43692  fourierdlem39  43694  fourierdlem40  43695  fourierdlem41  43696  fourierdlem42  43697  fourierdlem44  43699  fourierdlem47  43701  fourierdlem48  43702  fourierdlem49  43703  fourierdlem50  43704  fourierdlem51  43705  fourierdlem52  43706  fourierdlem54  43708  fourierdlem60  43714  fourierdlem61  43715  fourierdlem63  43717  fourierdlem64  43718  fourierdlem65  43719  fourierdlem73  43727  fourierdlem74  43728  fourierdlem75  43729  fourierdlem76  43730  fourierdlem78  43732  fourierdlem79  43733  fourierdlem81  43735  fourierdlem84  43738  fourierdlem87  43741  fourierdlem92  43746  fourierdlem93  43747  fourierdlem101  43755  fourierdlem102  43756  fourierdlem103  43757  fourierdlem104  43758  fourierdlem111  43765  fourierdlem114  43768  sqwvfoura  43776  sqwvfourb  43777  fouriersw  43779  etransclem19  43801  etransclem23  43805  etransclem24  43806  etransclem25  43807  etransclem27  43809  etransclem32  43814  etransclem35  43817  etransclem48  43830  qndenserrnbllem  43842  ioorrnopnlem  43852  ioorrnopnxrlem  43854  fsumlesge0  43922  sge0cl  43926  sge0supre  43934  sge0less  43937  sge0gerp  43940  sge0ltfirp  43945  sge0le  43952  sge0ltfirpmpt  43953  sge0split  43954  sge0rpcpnf  43966  sge0ltfirpmpt2  43971  sge0isum  43972  sge0xaddlem1  43978  sge0pnffigtmpt  43985  sge0pnffsumgt  43987  sge0gtfsumgt  43988  sge0seq  43991  nnfoctbdjlem  44000  meassle  44008  meaiuninclem  44025  meaiininclem  44031  omeiunle  44062  omeiunltfirp  44064  carageniuncllem2  44067  carageniuncl  44068  omess0  44079  hoicvr  44093  ovnlerp  44107  ovnsubaddlem1  44115  hsphoidmvle2  44130  hoidmv1lelem2  44137  hoidmv1le  44139  hoidmvlelem1  44140  hoidmvlelem2  44141  hoidmvlelem3  44142  hoidmvlelem5  44144  ovnhoilem2  44147  ovnhoi  44148  hoidifhspdmvle  44165  hoiqssbllem2  44168  hspmbllem2  44172  hspmbllem3  44173  hspmbl  44174  vonioolem2  44226  vonicclem2  44229  smfaddlem1  44308  smflimlem2  44317  smflimlem4  44319  smfmullem1  44336  smfinflem  44361  smflimsuplem4  44367  smflimsuplem8  44371  perfectALTVlem2  45185  nnpw2blen  45937  itscnhlinecirc02plem1  46139