Theorem breqtrd 4609

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

Syntax hints:   → wi 4   = wceq 1475   class class class wbr 4583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584

This theorem is referenced by:  breqtrrd  4611  syl5breq  4620  domunsn  7995  mapdom2  8016  phplem4  8027  mapfien2  8197  wemaplem2  8335  infdifsn  8437  cantnff  8454  infxpenlem  8719  pwcda1  8899  pwcdadom  8921  infmap2  8923  ssfin4  9015  canthp1lem1  9353  nqereq  9636  ltexnq  9676  ltbtwnnq  9679  add20  10419  mullt0  10426  ltm1  10742  recgt0  10746  prodgt0  10747  prodge0  10749  ltmul1a  10751  mulge0b  10772  recp1lt1  10800  recreclt  10801  ledivp1  10804  ledivp1i  10828  ltdivp1i  10829  eluzmn  11570  ltaddrp2d  11782  mul2lt0bi  11812  xleadd1a  11955  xov1plusxeqvd  12189  fz01en  12240  fzonmapblen  12381  fladdz  12488  flhalf  12493  fldiv  12521  modsubdir  12601  fzen2  12630  serle  12718  ltexp2a  12774  leexp2a  12778  exple1  12782  expubnd  12783  bernneq  12852  expmulnbnd  12858  discr1  12862  discr  12863  faclbnd6  12948  hashfz  13074  hashfun  13084  seqcoll  13105  sqeqd  13754  sqrlem7  13837  sqrtge0  13846  sqrtneglem  13855  abslt  13902  absle  13903  abstri  13918  rlimge0  14160  reccn2  14175  climaddc2  14214  isercolllem1  14243  caucvgrlem  14251  summolem2a  14293  isumge0  14339  fsumle  14372  fsumlt  14373  o1fsum  14386  supcvg  14427  expcnv  14435  geolim  14440  geolim2  14441  georeclim  14442  geo2lim  14445  mertenslem1  14455  mertens  14457  prodmolem2a  14503  efcllem  14647  ef0lem  14648  efgt0  14672  eftlub  14678  eflt  14686  sinbnd  14749  cosbnd  14750  ef01bndlem  14753  sin01gt0  14759  cos01gt0  14760  sin02gt0  14761  eirrlem  14771  rpnnen2lem11  14792  rpnnen2lem12  14793  ruclem11  14808  dvdssub2  14861  dvdsadd2b  14866  dvdsexp  14887  3dvds  14890  3dvdsOLD  14891  opoe  14925  bitsfzolem  14994  bitsinv1lem  15001  bezoutlem4  15097  dvdsgcd  15099  dvdsmulgcd  15112  bezoutr1  15120  nn0seqcvgd  15121  rpmulgcd2  15208  qredeq  15209  rpdvds  15212  prmind2  15236  divdenle  15295  hashdvds  15318  phimullem  15322  eulerthlem2  15325  prmdiveq  15329  prmdivdiv  15330  pythagtriplem4  15362  pythagtriplem10  15363  pythagtriplem19  15376  iserodd  15378  pcpre1  15385  pcadd2  15432  qexpz  15443  expnprm  15444  oddprmdvds  15445  pockthlem  15447  prmreclem2  15459  prmreclem3  15460  4sqlem7  15486  4sqlem10  15489  4sqlem11  15497  4sqlem12  15498  4sqlem14  15500  4sqlem15  15501  4sqlem16  15502  0ram  15562  ffthiso  16412  latmlej12  16914  qusgrp  17472  pgpfi1  17833  sylow1lem4  17839  sylow1lem5  17840  odcau  17842  pgpfi  17843  pgpssslw  17852  sylow3lem4  17868  sylow3lem6  17870  efgsfo  17975  frgp0  17996  odadd1  18074  odadd2  18075  odadd  18076  gexexlem  18078  lt6abl  18119  gsumzsubmcl  18141  pwsgsum  18201  dprd2dlem1  18263  dprd2d2  18266  ablfacrplem  18287  ablfacrp  18288  ablfacrp2  18289  ablfac1b  18292  ablfac1eu  18295  pgpfac1lem3a  18298  ablfaclem2  18308  dvdsrid  18474  dvdsrtr  18475  dvdsrneg  18477  unitmulcl  18487  unitgrp  18490  unitnegcl  18504  isdrng2  18580  subrguss  18618  subrgunit  18621  abvsubtri  18658  fidomndrnglem  19127  psrbaglesupp  19189  gzrngunit  19631  prmirredlem  19660  znidomb  19729  frlmgsum  19930  invrvald  20301  psmetsym  21925  psmettri  21926  mettri2  21956  xmetsym  21962  xmettri  21966  prdsxmetlem  21983  xblss2ps  22016  xblss2  22017  blhalf  22020  xmsge0  22078  ngptgp  22250  nrginvrcnlem  22305  nmoeq0  22350  cnmet  22385  blcvx  22409  opnreen  22442  metdcnlem  22447  metdstri  22462  metdsle  22463  metnrmlem1  22470  metnrmlem3  22472  lebnumlem1  22568  pi1inv  22660  cphnmf  22803  ipge0  22806  ipcau2  22841  tchcphlem1  22842  csbren  22990  minveclem2  23005  minveclem3  23008  ovolssnul  23062  ovolctb  23065  ovolunnul  23075  ovoliunlem1  23077  ovoliun2  23081  ovoliunnul  23082  ioombl1lem4  23136  uniioombllem3  23159  uniioombllem4  23160  uniioombllem5  23161  uniioombl  23163  volcn  23180  vitalilem2  23184  vitalilem5  23187  itg1lea  23285  mbfi1fseqlem6  23293  mbfi1flimlem  23295  itg2eqa  23318  itg2splitlem  23321  itg2split  23322  itg2monolem1  23323  itg2cnlem2  23335  iblabsr  23402  iblmulc2  23403  dveflem  23546  dvef  23547  dvferm2lem  23553  dvlip  23560  c1liplem1  23563  dveq0  23567  dvlt0  23572  dvivthlem1  23575  lhop1  23581  dvfsumle  23588  dvfsumlem4  23596  dvfsumrlim3  23600  dvfsum2  23601  ftc1a  23604  ftc1lem4  23606  deg1add  23667  ply1divex  23700  ply1rem  23727  fta1glem2  23730  fta1blem  23732  ig1pdvds  23740  plyeq0lem  23770  dgrcolem2  23834  plydivlem4  23855  plyrem  23864  fta1lem  23866  aalioulem3  23893  aaliou2b  23900  aaliou3lem3  23903  aaliou3lem8  23904  ulmcn  23957  ulmdvlem1  23958  itgulm  23966  pserulm  23980  pserdvlem2  23986  abelthlem2  23990  abelthlem5  23993  abelthlem6  23994  abelthlem7  23996  abelthlem8  23997  abelthlem9  23998  sinq12gt0  24063  sinq34lt0t  24065  cosq14gt0  24066  cosq14ge0  24067  efif1olem3  24094  argimgt0  24162  argimlt0  24163  logneg2  24165  logcnlem3  24190  logcnlem4  24191  logtayllem  24205  logtayl2  24208  cxpsqrtlem  24248  cxpsqrt  24249  cxpaddlelem  24292  abscxpbnd  24294  loglesqrt  24299  ang180lem2  24340  atanlogaddlem  24440  atanlogsublem  24442  atantan  24450  atans2  24458  atantayl  24464  leibpi  24469  log2tlbnd  24472  birthdaylem2  24479  birthdaylem3  24480  cxp2limlem  24502  jensenlem2  24514  jensen  24515  logdiflbnd  24521  emcllem2  24523  emcllem4  24525  harmonicbnd4  24537  fsumharmonic  24538  lgamgulmlem2  24556  lgamgulm2  24562  lgambdd  24563  lgamucov  24564  lgamcvglem  24566  lgamcvg2  24581  gamcvg  24582  wilthlem3  24596  basellem1  24607  basellem3  24609  basellem4  24610  fsumdvdsdiaglem  24709  dvdsppwf1o  24712  dvdsmulf1o  24720  chteq0  24734  chtub  24737  chpub  24745  logfacubnd  24746  logfaclbnd  24747  logexprlim  24750  perfectlem2  24755  dchrfi  24780  bclbnd  24805  bposlem1  24809  bposlem3  24811  bposlem4  24812  bposlem6  24814  lgslem1  24822  lgsqrlem2  24872  lgsqrlem4  24874  lgseisenlem2  24901  lgsquadlem1  24905  lgsquadlem2  24906  lgsquad2lem1  24909  2sqlem3  24945  2sqlem4  24946  2sqlem8  24951  2sqlem11  24954  chebbnd1lem2  24959  chebbnd1lem3  24960  chtppilimlem1  24962  chpchtlim  24968  vmadivsum  24971  vmadivsumb  24972  rpvmasumlem  24976  dchrisumlem2  24979  dchrmusum2  24983  dchrvmasumlem2  24987  dchrvmasumlem3  24988  dchrisum0flblem2  24998  dchrisum0fno1  25000  dchrisum0re  25002  dchrisum0lem1  25005  dchrisum0lem2a  25006  mudivsum  25019  mulogsumlem  25020  mulog2sumlem2  25024  vmalogdivsum2  25027  selberglem2  25035  selbergb  25038  selberg2b  25041  logdivbnd  25045  selberg3lem1  25046  selberg3lem2  25047  selberg4lem1  25049  pntrmax  25053  pntrlog2bndlem2  25067  pntrlog2bndlem3  25068  pntrlog2bndlem5  25070  pntrlog2bndlem6a  25071  pntrlog2bndlem6  25072  pntrlog2bnd  25073  pntpbnd1a  25074  pntpbnd1  25075  pntpbnd2  25076  pntibndlem1  25078  pntibndlem2  25080  pntlemb  25086  pntlemq  25090  pntlemr  25091  pntlemj  25092  pntlemk  25095  qabvle  25114  padicabvcxp  25121  ostth2lem2  25123  ostth2lem3  25124  ostth2lem4  25125  ostth3  25127  legtrid  25286  legov3  25293  krippenlem  25385  mideulem2  25426  midex  25429  opphllem5  25443  opphllem6  25444  opphl  25446  lmieu  25476  lmiisolem  25488  ttgcontlem1  25565  colinearalglem4  25589  axpaschlem  25620  axcontlem7  25650  clwlkndivn  26380  nvge0  26912  smcnlem  26936  nmoub3i  27012  nmoub2i  27013  nmlno0lem  27032  minvecolem2  27115  htthlem  27158  norm3dif2  27392  bcs2  27423  chscllem2  27881  eigposi  28079  nmopub2tALT  28152  nmfnleub2  28169  nmlnop0iALT  28238  riesz1  28308  cnlnadjlem2  28311  nmopcoadji  28344  leopsq  28372  leopmul  28377  leopnmid  28381  nmopleid  28382  opsqrlem6  28388  0leopj  28429  hstle1  28469  strlem3a  28495  mdslmd4i  28576  cvexchlem  28611  cdj1i  28676  le2halvesd  28910  xlt2addrd  28913  2sqcoprm  28978  2sqmod  28979  archiabllem1a  29076  archiabllem2a  29079  archiabllem2c  29080  xrge0tsmsd  29116  orngsqr  29135  ornglmulle  29136  orngrmulle  29137  orng0le1  29143  fzto1st1  29183  metideq  29264  metider  29265  sqsscirc1  29282  esummono  29443  esumpad2  29445  esumle  29447  esumlef  29451  esumcst  29452  esumrnmpt2  29457  esum2d  29482  aean  29634  dya2ub  29659  dya2icoseg  29666  omssubadd  29689  inelcarsg  29700  carsgsigalem  29704  carsggect  29707  carsgclctunlem2  29708  eulerpartlemb  29757  fibp1  29790  sgnmulsgp  29939  signsplypnf  29953  signsply0  29954  subfacval3  30425  sconpht2  30474  sconpi1  30475  rescon  30482  snmlff  30565  sinccvglem  30820  faclimlem2  30883  btwnouttr2  31299  dnibndlem5  31642  dnibndlem7  31644  dnibndlem8  31645  dnibndlem9  31646  dnibndlem10  31647  dnibnd  31651  knoppcnlem4  31656  knoppcnlem9  31661  unbdqndv2lem1  31670  unbdqndv2lem2  31671  knoppndvlem11  31683  knoppndvlem12  31684  knoppndvlem14  31686  knoppndvlem15  31687  knoppndvlem17  31689  knoppndvlem18  31690  knoppndvlem19  31691  knoppndvlem21  31693  ltflcei  32567  poimirlem9  32588  poimirlem26  32605  poimirlem27  32606  poimirlem29  32608  heicant  32614  mblfinlem2  32617  mblfinlem3  32618  mblfinlem4  32619  volsupnfl  32624  itg2addnclem  32631  itg2addnclem3  32633  iblmulc2nc  32645  bddiblnc  32650  ftc1cnnclem  32653  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anclem8  32662  ftc2nc  32664  dvasin  32666  geomcau  32725  bfplem2  32792  rrncmslem  32801  rrnequiv  32804  lsatcvatlem  33354  islshpcv  33358  atlatmstc  33624  cvlsupr7  33653  cvrval3  33717  cvrval5  33719  cvrexchlem  33723  atcvrj1  33735  cvrat3  33746  cvrat4  33747  atbtwn  33750  1cvratex  33777  hlatexch4  33785  3atlem1  33787  3atlem2  33788  atcvrlln2  33823  atcvrlln  33824  lplnllnneN  33860  llncvrlpln2  33861  4atlem3b  33902  lplncvrlvol2  33919  dalemswapyz  33960  dalemswapyzps  33994  dalem25  34002  dalem39  34015  dalem58  34034  dalem59  34035  lneq2at  34082  lncvrat  34086  dalawlem2  34176  dalawlem3  34177  dalawlem4  34178  dalawlem6  34180  dalawlem9  34183  dalawlem11  34185  dalawlem12  34186  lhpocnle  34320  lhpmcvr3  34329  lhpmcvr5N  34331  lhpmcvr6N  34332  4atexlemunv  34370  4atexlemc  34373  4atexlemex2  34375  lautm  34398  cdlemc2  34497  cdleme5  34545  cdleme11j  34572  cdleme16b  34584  cdlemednpq  34604  cdleme19e  34613  cdleme20i  34623  cdleme22a  34646  cdleme22cN  34648  cdleme22d  34649  cdleme22e  34650  cdleme22eALTN  34651  cdleme22f  34652  cdleme23c  34657  cdleme30a  34684  cdleme35a  34754  cdleme35b  34756  cdleme42h  34788  cdlemeg46rgv  34834  cdlemg8b  34934  cdlemg12e  34953  cdlemg13a  34957  cdlemg17pq  34978  cdlemg18c  34986  cdlemg19  34990  cdlemg21  34992  cdlemg31d  35006  cdlemg33a  35012  tendoid  35079  cdlemk4  35140  cdlemki  35147  cdlemk10  35149  cdlemksv2  35153  cdlemk12  35156  cdlemk14  35160  cdlemk15  35161  cdlemk1u  35165  cdlemk5u  35167  cdlemk12u  35178  cdlemk45  35253  cdlemk48  35256  dia2dimlem1  35371  dia2dimlem2  35372  dia2dimlem3  35373  cdlemm10N  35425  cdlemn2  35502  dihjustlem  35523  dihglbcpreN  35607  dihmeetlem3N  35612  irrapxlem1  36404  pell1qrgaplem  36455  pell1qrgap  36456  monotoddzzfi  36525  jm2.24nn  36544  congtr  36550  congmul  36552  congsub  36555  fzmaxdif  36566  acongeq  36568  jm2.20nn  36582  jm2.25  36584  hbtlem4  36715  dgrsub2  36724  mpaaeu  36739  idomsubgmo  36795  int-sqgeq0d  37511  int-ineqmvtd  37516  cvgdvgrat  37534  radcnvrat  37535  hashnzfzclim  37543  dvconstbi  37555  binomcxplemdvbinom  37574  isosctrlem1ALT  38192  mulltgt0  38204  oddfl  38430  2timesgt  38441  lt3addmuld  38456  lt4addmuld  38461  supxrgere  38490  supxrgelem  38494  supxrge  38495  xadd0ge2  38498  infrpge  38508  xrlexaddrp  38509  xralrple2  38511  infxr  38524  infleinflem1  38527  infleinflem2  38528  infleinf  38529  xralrple4  38530  xralrple3  38531  recnnltrp  38534  rpgtrecnn  38538  xrralrecnnge  38554  iccshift  38591  iooshift  38595  ressiocsup  38628  ressioosup  38629  fsumnncl  38638  fmul01  38647  fmul01lt1lem1  38651  fmul01lt1lem2  38652  mccllem  38664  climrec  38670  climexp  38672  climneg  38677  limcrecl  38696  sumnnodd  38697  lptioo2  38698  lptioo1  38699  ltmod  38705  lptre2pt  38707  0ellimcdiv  38716  limclner  38718  fnlimcnv  38734  cncficcgt0  38774  cncfioobdlem  38782  ioodvbdlimc1lem1  38821  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvdsn1add  38829  dvnxpaek  38832  dvnmul  38833  dvnprodlem1  38836  itgiccshift  38872  itgperiod  38873  sublevolico  38877  ismbl3  38879  ovolsplit  38881  ismbl4  38886  stoweidlem1  38894  stoweidlem11  38904  stoweidlem13  38906  stoweidlem26  38919  stoweidlem34  38927  stoweidlem38  38931  stoweidlem42  38935  stoweidlem51  38944  stoweidlem59  38952  stirlinglem5  38971  stirlinglem6  38972  stirlinglem7  38973  stirlinglem10  38976  stirlinglem11  38977  stirlinglem13  38979  stirlinglem15  38981  dirkercncflem1  38996  dirkercncflem4  38999  fourierdlem4  39004  fourierdlem10  39010  fourierdlem11  39011  fourierdlem15  39015  fourierdlem20  39020  fourierdlem25  39025  fourierdlem26  39026  fourierdlem30  39030  fourierdlem37  39037  fourierdlem39  39039  fourierdlem40  39040  fourierdlem41  39041  fourierdlem42  39042  fourierdlem44  39044  fourierdlem47  39046  fourierdlem48  39047  fourierdlem49  39048  fourierdlem50  39049  fourierdlem51  39050  fourierdlem52  39051  fourierdlem54  39053  fourierdlem60  39059  fourierdlem61  39060  fourierdlem63  39062  fourierdlem64  39063  fourierdlem65  39064  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem78  39077  fourierdlem79  39078  fourierdlem81  39080  fourierdlem84  39083  fourierdlem87  39086  fourierdlem92  39091  fourierdlem93  39092  fourierdlem101  39100  fourierdlem102  39101  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  fourierdlem114  39113  sqwvfoura  39121  sqwvfourb  39122  fouriersw  39124  etransclem19  39146  etransclem23  39150  etransclem24  39151  etransclem25  39152  etransclem27  39154  etransclem32  39159  etransclem35  39162  etransclem48  39175  qndenserrnbllem  39190  ioorrnopnlem  39200  ioorrnopnxrlem  39202  fsumlesge0  39270  sge0cl  39274  sge0supre  39282  sge0less  39285  sge0gerp  39288  sge0ltfirp  39293  sge0le  39300  sge0ltfirpmpt  39301  sge0split  39302  sge0rpcpnf  39314  sge0ltfirpmpt2  39319  sge0isum  39320  sge0xaddlem1  39326  sge0pnffigtmpt  39333  sge0pnffsumgt  39335  sge0gtfsumgt  39336  sge0seq  39339  nnfoctbdjlem  39348  meassle  39356  meaiuninclem  39373  meaiininclem  39376  omeiunle  39407  omeiunltfirp  39409  carageniuncllem2  39412  carageniuncl  39413  omess0  39424  hoicvr  39438  ovnlerp  39452  ovnsubaddlem1  39460  hsphoidmvle2  39475  hoidmv1lelem2  39482  hoidmv1le  39484  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvlelem5  39489  ovnhoilem2  39492  ovnhoi  39493  hoidifhspdmvle  39510  hoiqssbllem2  39513  hspmbllem2  39517  hspmbllem3  39518  hspmbl  39519  vonioolem2  39572  vonicclem2  39575  smfaddlem1  39649  smflimlem2  39658  smflimlem4  39660  smfmullem1  39676  perfectALTVlem2  40165  nbfusgrlevtxm2  40606  clwlksndivn  41279  eucrct2eupth  41413  frgrwopreglem2  41482  nnpw2blen  42172