Theorem breqtrd 4679

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

Syntax hints:   → wi 4   = wceq 1483   class class class wbr 4653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654

This theorem is referenced by:  breqtrrd  4681  syl5breq  4690  domunsn  8110  mapdom2  8131  phplem4  8142  mapfien2  8314  wemaplem2  8452  infdifsn  8554  cantnff  8571  infxpenlem  8836  pwcda1  9016  pwcdadom  9038  infmap2  9040  ssfin4  9132  canthp1lem1  9474  nqereq  9757  ltexnq  9797  ltbtwnnq  9800  add20  10540  mullt0  10547  ltm1  10863  recgt0  10867  prodgt0  10868  prodge0  10870  ltmul1a  10872  mulge0b  10893  recp1lt1  10921  recreclt  10922  ledivp1  10925  ledivp1i  10949  ltdivp1i  10950  eluzmn  11694  ltaddrp2d  11906  mul2lt0bi  11936  xleadd1a  12083  xov1plusxeqvd  12318  fz01en  12369  fzonmapblen  12513  fladdz  12626  flhalf  12631  fldiv  12659  modsubdir  12739  fzen2  12768  serle  12856  ltexp2a  12912  leexp2a  12916  exple1  12920  expubnd  12921  bernneq  12990  expmulnbnd  12996  discr1  13000  discr  13001  faclbnd6  13086  hashfz  13214  hashfun  13224  seqcoll  13248  sqeqd  13906  sqrlem7  13989  sqrtge0  13998  sqrtneglem  14007  abslt  14054  absle  14055  abstri  14070  rlimge0  14312  reccn2  14327  climaddc2  14366  isercolllem1  14395  caucvgrlem  14403  summolem2a  14446  isumge0  14497  fsumle  14531  fsumlt  14532  o1fsum  14545  supcvg  14588  expcnv  14596  geolim  14601  geolim2  14602  georeclim  14603  geo2lim  14606  mertenslem1  14616  mertens  14618  prodmolem2a  14664  efcllem  14808  ef0lem  14809  efgt0  14833  eftlub  14839  eflt  14847  sinbnd  14910  cosbnd  14911  ef01bndlem  14914  sin01gt0  14920  cos01gt0  14921  sin02gt0  14922  eirrlem  14932  rpnnen2lem11  14953  rpnnen2lem12  14954  ruclem11  14969  dvdssub2  15023  dvdsadd2b  15028  dvdsexp  15049  3dvds  15052  3dvdsOLD  15053  opoe  15087  bitsfzolem  15156  bitsinv1lem  15163  bezoutlem4  15259  dvdsgcd  15261  dvdsmulgcd  15274  bezoutr1  15282  nn0seqcvgd  15283  rpmulgcd2  15370  qredeq  15371  rpdvds  15374  prmind2  15398  divdenle  15457  hashdvds  15480  phimullem  15484  eulerthlem2  15487  prmdiveq  15491  prmdivdiv  15492  pythagtriplem4  15524  pythagtriplem10  15525  pythagtriplem19  15538  iserodd  15540  pcpre1  15547  pcadd2  15594  qexpz  15605  expnprm  15606  oddprmdvds  15607  pockthlem  15609  prmreclem2  15621  prmreclem3  15622  4sqlem7  15648  4sqlem10  15651  4sqlem11  15659  4sqlem12  15660  4sqlem14  15662  4sqlem15  15663  4sqlem16  15664  0ram  15724  ffthiso  16589  latmlej12  17091  qusgrp  17649  pgpfi1  18010  sylow1lem4  18016  sylow1lem5  18017  odcau  18019  pgpfi  18020  pgpssslw  18029  sylow3lem4  18045  sylow3lem6  18047  efgsfo  18152  frgp0  18173  odadd1  18251  odadd2  18252  odadd  18253  gexexlem  18255  lt6abl  18296  gsumzsubmcl  18318  pwsgsum  18378  dprd2dlem1  18440  dprd2d2  18443  ablfacrplem  18464  ablfacrp  18465  ablfacrp2  18466  ablfac1b  18469  ablfac1eu  18472  pgpfac1lem3a  18475  ablfaclem2  18485  dvdsrid  18651  dvdsrtr  18652  dvdsrneg  18654  unitmulcl  18664  unitgrp  18667  unitnegcl  18681  isdrng2  18757  subrguss  18795  subrgunit  18798  abvsubtri  18835  fidomndrnglem  19306  psrbaglesupp  19368  gzrngunit  19812  prmirredlem  19841  znidomb  19910  frlmgsum  20111  invrvald  20482  psmetsym  22115  psmettri  22116  mettri2  22146  xmetsym  22152  xmettri  22156  prdsxmetlem  22173  xblss2ps  22206  xblss2  22207  blhalf  22210  xmsge0  22268  ngptgp  22440  nrginvrcnlem  22495  nmoeq0  22540  cnmet  22575  blcvx  22601  opnreen  22634  metdcnlem  22639  metdstri  22654  metdsle  22655  metnrmlem1  22662  metnrmlem3  22664  lebnumlem1  22760  pi1inv  22852  cphnmf  22995  ipge0  22998  ipcau2  23033  tchcphlem1  23034  csbren  23182  minveclem2  23197  minveclem3  23200  ovolssnul  23255  ovolctb  23258  ovolunnul  23268  ovoliunlem1  23270  ovoliun2  23274  ovoliunnul  23275  ioombl1lem4  23329  uniioombllem3  23353  uniioombllem4  23354  uniioombllem5  23355  uniioombl  23357  volcn  23374  vitalilem2  23378  vitalilem5  23381  itg1lea  23479  mbfi1fseqlem6  23487  mbfi1flimlem  23489  itg2eqa  23512  itg2splitlem  23515  itg2split  23516  itg2monolem1  23517  itg2cnlem2  23529  iblabsr  23596  iblmulc2  23597  dveflem  23742  dvef  23743  dvferm2lem  23749  dvlip  23756  c1liplem1  23759  dveq0  23763  dvlt0  23768  dvivthlem1  23771  lhop1  23777  dvfsumle  23784  dvfsumlem4  23792  dvfsumrlim3  23796  dvfsum2  23797  ftc1a  23800  ftc1lem4  23802  deg1add  23863  ply1divex  23896  ply1rem  23923  fta1glem2  23926  fta1blem  23928  ig1pdvds  23936  plyeq0lem  23966  dgrcolem2  24030  plydivlem4  24051  plyrem  24060  fta1lem  24062  aalioulem3  24089  aaliou2b  24096  aaliou3lem3  24099  aaliou3lem8  24100  ulmcn  24153  ulmdvlem1  24154  itgulm  24162  pserulm  24176  pserdvlem2  24182  abelthlem2  24186  abelthlem5  24189  abelthlem6  24190  abelthlem7  24192  abelthlem8  24193  abelthlem9  24194  sinq12gt0  24259  sinq34lt0t  24261  cosq14gt0  24262  cosq14ge0  24263  efif1olem3  24290  argimgt0  24358  argimlt0  24359  logneg2  24361  logcnlem3  24390  logcnlem4  24391  logtayllem  24405  logtayl2  24408  cxpsqrtlem  24448  cxpsqrt  24449  cxpaddlelem  24492  abscxpbnd  24494  loglesqrt  24499  ang180lem2  24540  atanlogaddlem  24640  atanlogsublem  24642  atantan  24650  atans2  24658  atantayl  24664  leibpi  24669  log2tlbnd  24672  birthdaylem2  24679  birthdaylem3  24680  cxp2limlem  24702  jensenlem2  24714  jensen  24715  logdiflbnd  24721  emcllem2  24723  emcllem4  24725  harmonicbnd4  24737  fsumharmonic  24738  lgamgulmlem2  24756  lgamgulm2  24762  lgambdd  24763  lgamucov  24764  lgamcvglem  24766  lgamcvg2  24781  gamcvg  24782  wilthlem3  24796  basellem1  24807  basellem3  24809  basellem4  24810  fsumdvdsdiaglem  24909  dvdsppwf1o  24912  dvdsmulf1o  24920  chteq0  24934  chtub  24937  chpub  24945  logfacubnd  24946  logfaclbnd  24947  logexprlim  24950  perfectlem2  24955  dchrfi  24980  bclbnd  25005  bposlem1  25009  bposlem3  25011  bposlem4  25012  bposlem6  25014  lgslem1  25022  lgsqrlem2  25072  lgsqrlem4  25074  lgseisenlem2  25101  lgsquadlem1  25105  lgsquadlem2  25106  lgsquad2lem1  25109  2sqlem3  25145  2sqlem4  25146  2sqlem8  25151  2sqlem11  25154  chebbnd1lem2  25159  chebbnd1lem3  25160  chtppilimlem1  25162  chpchtlim  25168  vmadivsum  25171  vmadivsumb  25172  rpvmasumlem  25176  dchrisumlem2  25179  dchrmusum2  25183  dchrvmasumlem2  25187  dchrvmasumlem3  25188  dchrisum0flblem2  25198  dchrisum0fno1  25200  dchrisum0re  25202  dchrisum0lem1  25205  dchrisum0lem2a  25206  mudivsum  25219  mulogsumlem  25220  mulog2sumlem2  25224  vmalogdivsum2  25227  selberglem2  25235  selbergb  25238  selberg2b  25241  logdivbnd  25245  selberg3lem1  25246  selberg3lem2  25247  selberg4lem1  25249  pntrmax  25253  pntrlog2bndlem2  25267  pntrlog2bndlem3  25268  pntrlog2bndlem5  25270  pntrlog2bndlem6a  25271  pntrlog2bndlem6  25272  pntrlog2bnd  25273  pntpbnd1a  25274  pntpbnd1  25275  pntpbnd2  25276  pntibndlem1  25278  pntibndlem2  25280  pntlemb  25286  pntlemq  25290  pntlemr  25291  pntlemj  25292  pntlemk  25295  qabvle  25314  padicabvcxp  25321  ostth2lem2  25323  ostth2lem3  25324  ostth2lem4  25325  ostth3  25327  legtrid  25486  legov3  25493  krippenlem  25585  mideulem2  25626  midex  25629  opphllem5  25643  opphllem6  25644  opphl  25646  lmieu  25676  lmiisolem  25688  ttgcontlem1  25765  colinearalglem4  25789  axpaschlem  25820  axcontlem7  25850  nbfusgrlevtxm2  26280  clwlksndivn  26972  eucrct2eupth  27105  nvge0  27528  smcnlem  27552  nmoub3i  27628  nmoub2i  27629  nmlno0lem  27648  minvecolem2  27731  htthlem  27774  norm3dif2  28008  bcs2  28039  chscllem2  28497  eigposi  28695  nmopub2tALT  28768  nmfnleub2  28785  nmlnop0iALT  28854  riesz1  28924  cnlnadjlem2  28927  nmopcoadji  28960  leopsq  28988  leopmul  28993  leopnmid  28997  nmopleid  28998  opsqrlem6  29004  0leopj  29045  hstle1  29085  strlem3a  29111  mdslmd4i  29192  cvexchlem  29227  cdj1i  29292  le2halvesd  29520  xlt2addrd  29523  fsumub  29574  2sqcoprm  29647  2sqmod  29648  archiabllem1a  29745  archiabllem2a  29748  archiabllem2c  29749  xrge0tsmsd  29785  orngsqr  29804  ornglmulle  29805  orngrmulle  29806  orng0le1  29812  fzto1st1  29852  metideq  29936  metider  29937  sqsscirc1  29954  esummono  30116  esumpad2  30118  esumle  30120  esumlef  30124  esumcst  30125  esumrnmpt2  30130  esum2d  30155  aean  30307  dya2ub  30332  dya2icoseg  30339  omssubadd  30362  inelcarsg  30373  carsgsigalem  30377  carsggect  30380  carsgclctunlem2  30381  eulerpartlemb  30430  fibp1  30463  sgnmulsgp  30612  signsplypnf  30627  signsply0  30628  fdvposlt  30677  fdvposle  30679  reprgt  30699  logdivsqrle  30728  hgt750lemb  30734  hgt750leme  30736  tgoldbachgtde  30738  subfacval3  31171  sconnpht2  31220  sconnpi1  31221  resconn  31228  snmlff  31311  sinccvglem  31566  faclimlem2  31630  btwnouttr2  32129  dnibndlem5  32472  dnibndlem7  32474  dnibndlem8  32475  dnibndlem9  32476  dnibndlem10  32477  dnibnd  32481  knoppcnlem4  32486  knoppcnlem9  32491  unbdqndv2lem1  32500  unbdqndv2lem2  32501  knoppndvlem11  32513  knoppndvlem12  32514  knoppndvlem14  32516  knoppndvlem15  32517  knoppndvlem17  32519  knoppndvlem18  32520  knoppndvlem19  32521  knoppndvlem21  32523  ltflcei  33397  poimirlem9  33418  poimirlem26  33435  poimirlem27  33436  poimirlem29  33438  heicant  33444  mblfinlem2  33447  mblfinlem3  33448  mblfinlem4  33449  volsupnfl  33454  itg2addnclem  33461  itg2addnclem3  33463  iblmulc2nc  33475  bddiblnc  33480  ftc1cnnclem  33483  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anclem8  33492  ftc2nc  33494  dvasin  33496  geomcau  33555  bfplem2  33622  rrncmslem  33631  rrnequiv  33634  lsatcvatlem  34336  islshpcv  34340  atlatmstc  34606  cvlsupr7  34635  cvrval3  34699  cvrval5  34701  cvrexchlem  34705  atcvrj1  34717  cvrat3  34728  cvrat4  34729  atbtwn  34732  1cvratex  34759  hlatexch4  34767  3atlem1  34769  3atlem2  34770  atcvrlln2  34805  atcvrlln  34806  lplnllnneN  34842  llncvrlpln2  34843  4atlem3b  34884  lplncvrlvol2  34901  dalemswapyz  34942  dalemswapyzps  34976  dalem25  34984  dalem39  34997  dalem58  35016  dalem59  35017  lneq2at  35064  lncvrat  35068  dalawlem2  35158  dalawlem3  35159  dalawlem4  35160  dalawlem6  35162  dalawlem9  35165  dalawlem11  35167  dalawlem12  35168  lhpocnle  35302  lhpmcvr3  35311  lhpmcvr5N  35313  lhpmcvr6N  35314  4atexlemunv  35352  4atexlemc  35355  4atexlemex2  35357  lautm  35380  cdlemc2  35479  cdleme5  35527  cdleme11j  35554  cdleme16b  35566  cdlemednpq  35586  cdleme19e  35595  cdleme20i  35605  cdleme22a  35628  cdleme22cN  35630  cdleme22d  35631  cdleme22e  35632  cdleme22eALTN  35633  cdleme22f  35634  cdleme23c  35639  cdleme30a  35666  cdleme35a  35736  cdleme35b  35738  cdleme42h  35770  cdlemeg46rgv  35816  cdlemg8b  35916  cdlemg12e  35935  cdlemg13a  35939  cdlemg17pq  35960  cdlemg18c  35968  cdlemg19  35972  cdlemg21  35974  cdlemg31d  35988  cdlemg33a  35994  tendoid  36061  cdlemk4  36122  cdlemki  36129  cdlemk10  36131  cdlemksv2  36135  cdlemk12  36138  cdlemk14  36142  cdlemk15  36143  cdlemk1u  36147  cdlemk5u  36149  cdlemk12u  36160  cdlemk45  36235  cdlemk48  36238  dia2dimlem1  36353  dia2dimlem2  36354  dia2dimlem3  36355  cdlemm10N  36407  cdlemn2  36484  dihjustlem  36505  dihglbcpreN  36589  dihmeetlem3N  36594  irrapxlem1  37386  pell1qrgaplem  37437  pell1qrgap  37438  monotoddzzfi  37507  jm2.24nn  37526  congtr  37532  congmul  37534  congsub  37537  fzmaxdif  37548  acongeq  37550  jm2.20nn  37564  jm2.25  37566  hbtlem4  37696  dgrsub2  37705  mpaaeu  37720  idomsubgmo  37776  leeq2d  38456  int-sqgeq0d  38489  int-ineqmvtd  38494  cvgdvgrat  38512  radcnvrat  38513  hashnzfzclim  38521  dvconstbi  38533  binomcxplemdvbinom  38552  isosctrlem1ALT  39170  mulltgt0  39181  rnmptbd2lem  39463  oddfl  39489  2timesgt  39500  lt3addmuld  39515  lt4addmuld  39520  supxrgere  39549  supxrgelem  39553  supxrge  39554  xadd0ge2  39557  infrpge  39567  xrlexaddrp  39568  xralrple2  39570  infxr  39583  infleinflem1  39586  infleinflem2  39587  infleinf  39588  xralrple4  39589  xralrple3  39590  recnnltrp  39593  rpgtrecnn  39597  xrralrecnnge  39613  rexabslelem  39645  infrnmptle  39650  supminfxr  39694  iccshift  39744  iooshift  39748  ressiocsup  39781  ressioosup  39782  fsumnncl  39803  fmul01  39812  fmul01lt1lem1  39816  fmul01lt1lem2  39817  mccllem  39829  climrec  39835  climexp  39837  climneg  39842  limcrecl  39861  sumnnodd  39862  lptioo2  39863  lptioo1  39864  ltmod  39870  lptre2pt  39872  0ellimcdiv  39881  limclner  39883  fnlimcnv  39899  climinf2lem  39938  limsupubuzlem  39944  limsup10exlem  40004  limsupgtlem  40009  dfxlim2v  40073  cncficcgt0  40101  cncfioobdlem  40109  ioodvbdlimc1lem1  40146  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvdsn1add  40154  dvnxpaek  40157  dvnmul  40158  dvnprodlem1  40161  itgiccshift  40196  itgperiod  40197  sublevolico  40201  ismbl3  40203  ovolsplit  40205  ismbl4  40210  stoweidlem1  40218  stoweidlem11  40228  stoweidlem13  40230  stoweidlem26  40243  stoweidlem34  40251  stoweidlem38  40255  stoweidlem42  40259  stoweidlem51  40268  stoweidlem59  40276  stirlinglem5  40295  stirlinglem6  40296  stirlinglem7  40297  stirlinglem10  40300  stirlinglem11  40301  stirlinglem13  40303  stirlinglem15  40305  dirkercncflem1  40320  dirkercncflem4  40323  fourierdlem4  40328  fourierdlem10  40334  fourierdlem11  40335  fourierdlem15  40339  fourierdlem20  40344  fourierdlem25  40349  fourierdlem26  40350  fourierdlem30  40354  fourierdlem37  40361  fourierdlem39  40363  fourierdlem40  40364  fourierdlem41  40365  fourierdlem42  40366  fourierdlem44  40368  fourierdlem47  40370  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  fourierdlem51  40374  fourierdlem52  40375  fourierdlem54  40377  fourierdlem60  40383  fourierdlem61  40384  fourierdlem63  40386  fourierdlem64  40387  fourierdlem65  40388  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem78  40401  fourierdlem79  40402  fourierdlem81  40404  fourierdlem84  40407  fourierdlem87  40410  fourierdlem92  40415  fourierdlem93  40416  fourierdlem101  40424  fourierdlem102  40425  fourierdlem103  40426  fourierdlem104  40427  fourierdlem111  40434  fourierdlem114  40437  sqwvfoura  40445  sqwvfourb  40446  fouriersw  40448  etransclem19  40470  etransclem23  40474  etransclem24  40475  etransclem25  40476  etransclem27  40478  etransclem32  40483  etransclem35  40486  etransclem48  40499  qndenserrnbllem  40514  ioorrnopnlem  40524  ioorrnopnxrlem  40526  fsumlesge0  40594  sge0cl  40598  sge0supre  40606  sge0less  40609  sge0gerp  40612  sge0ltfirp  40617  sge0le  40624  sge0ltfirpmpt  40625  sge0split  40626  sge0rpcpnf  40638  sge0ltfirpmpt2  40643  sge0isum  40644  sge0xaddlem1  40650  sge0pnffigtmpt  40657  sge0pnffsumgt  40659  sge0gtfsumgt  40660  sge0seq  40663  nnfoctbdjlem  40672  meassle  40680  meaiuninclem  40697  meaiininclem  40700  omeiunle  40731  omeiunltfirp  40733  carageniuncllem2  40736  carageniuncl  40737  omess0  40748  hoicvr  40762  ovnlerp  40776  ovnsubaddlem1  40784  hsphoidmvle2  40799  hoidmv1lelem2  40806  hoidmv1le  40808  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvlelem5  40813  ovnhoilem2  40816  ovnhoi  40817  hoidifhspdmvle  40834  hoiqssbllem2  40837  hspmbllem2  40841  hspmbllem3  40842  hspmbl  40843  vonioolem2  40895  vonicclem2  40898  smfaddlem1  40971  smflimlem2  40980  smflimlem4  40982  smfmullem1  40998  smfinflem  41023  smflimsuplem4  41029  smflimsuplem8  41033  perfectALTVlem2  41631  nnpw2blen  42374