Theorem breqtrd 4952

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

Syntax hints:   → wi 4   = wceq 1508   class class class wbr 4926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-rab 3092  df-v 3412  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-nul 4174  df-if 4346  df-sn 4437  df-pr 4439  df-op 4443  df-br 4927

This theorem is referenced by:  breqtrrd  4954  syl5breq  4963  domunsn  8462  mapdom2  8483  phplem4  8494  mapfien2  8666  wemaplem2  8805  infdifsn  8913  cantnff  8930  infxpenlem  9232  infmap2  9437  ssfin4  9529  canthp1lem1  9871  nqereq  10154  ltexnq  10194  ltbtwnnq  10197  add20  10952  mullt0  10959  ltm1  11282  recgt0  11286  prodgt0  11287  ltmul1a  11289  mulge0b  11310  recp1lt1  11338  recreclt  11339  ledivp1  11342  ledivp1i  11365  ltdivp1i  11366  eluzmn  12064  ltaddrp2d  12281  mul2lt0bi  12311  prodge0rd  12312  xleadd1a  12461  xov1plusxeqvd  12699  fz01en  12750  fzonmapblen  12897  fladdz  13009  flhalf  13014  fldiv  13042  modsubdir  13122  fzen2  13151  serle  13239  ltexp2a  13344  leexp2a  13350  exple1  13354  expubnd  13355  bernneq  13404  expmulnbnd  13410  discr1  13414  discr  13415  faclbnd6  13473  hashfz  13600  hashfun  13610  seqcoll  13634  sqeqd  14385  sqrlem7  14468  sqrtge0  14477  sqrtneglem  14486  abslt  14534  absle  14535  abstri  14550  rlimge0  14798  reccn2  14813  climaddc2  14852  isercolllem1  14881  caucvgrlem  14889  summolem2a  14931  isumge0  14980  fsumle  15013  fsumlt  15014  o1fsum  15027  supcvg  15070  expcnv  15078  geolim  15085  geolim2  15086  georeclim  15087  geo2lim  15090  mertenslem1  15099  mertens  15101  prodmolem2a  15147  efcllem  15290  ef0lem  15291  efgt0  15315  eftlub  15321  eflt  15329  sinbnd  15392  cosbnd  15393  ef01bndlem  15396  sin01gt0  15402  cos01gt0  15403  sin02gt0  15404  eirrlem  15416  rpnnen2lem11  15436  rpnnen2lem12  15437  ruclem11  15452  dvdssub2  15510  dvdsadd2b  15515  dvdsexp  15536  3dvds  15539  opoe  15571  bitsfzolem  15642  bitsinv1lem  15649  bezoutlem4  15745  dvdsgcd  15747  dvdsmulgcd  15760  bezoutr1  15768  nn0seqcvgd  15769  rpmulgcd2  15855  qredeq  15856  rpdvds  15859  prmind2  15884  divdenle  15944  hashdvds  15967  phimullem  15971  eulerthlem2  15974  prmdiveq  15978  prmdivdiv  15979  pythagtriplem4  16011  pythagtriplem10  16012  pythagtriplem19  16025  iserodd  16027  pcpre1  16034  pcadd2  16081  qexpz  16092  expnprm  16093  oddprmdvds  16094  pockthlem  16096  prmreclem2  16108  prmreclem3  16109  4sqlem7  16135  4sqlem10  16138  4sqlem11  16146  4sqlem12  16147  4sqlem14  16149  4sqlem15  16150  4sqlem16  16151  0ram  16211  ffthiso  17070  latmlej12  17572  qusgrp  18131  pgpfi1  18494  sylow1lem4  18500  sylow1lem5  18501  odcau  18503  pgpfi  18504  pgpssslw  18513  sylow3lem4  18529  sylow3lem6  18531  efgsfo  18637  frgp0  18659  odadd1  18737  odadd2  18738  odadd  18739  gexexlem  18741  lt6abl  18782  gsumzsubmcl  18804  pwsgsum  18865  dprd2dlem1  18926  dprd2d2  18929  ablfacrplem  18950  ablfacrp  18951  ablfacrp2  18952  ablfac1b  18955  ablfac1eu  18958  pgpfac1lem3a  18961  ablfaclem2  18971  dvdsrid  19137  dvdsrtr  19138  dvdsrneg  19140  unitmulcl  19150  unitgrp  19153  unitnegcl  19167  isdrng2  19248  subrguss  19286  subrgunit  19289  abvsubtri  19341  fidomndrnglem  19813  psrbaglesupp  19875  gzrngunit  20329  prmirredlem  20358  znidomb  20426  frlmgsum  20634  invrvald  21005  psmetsym  22639  psmettri  22640  mettri2  22670  xmetsym  22676  xmettri  22680  prdsxmetlem  22697  xblss2ps  22730  xblss2  22731  blhalf  22734  xmsge0  22792  ngptgp  22964  nrginvrcnlem  23019  nmoeq0  23064  cnmet  23099  blcvx  23125  opnreen  23158  metdcnlem  23163  metdstri  23178  metdsle  23179  metnrmlem1  23186  metnrmlem3  23188  lebnumlem1  23284  pi1inv  23375  cphnmf  23518  ipge0  23521  ipcau2  23556  tcphcphlem1  23557  csbren  23721  minveclem2  23748  minveclem3  23751  ovolssnul  23807  ovolctb  23810  ovolunnul  23820  ovoliunlem1  23822  ovoliun2  23826  ovoliunnul  23827  ioombl1lem4  23881  uniioombllem3  23905  uniioombllem4  23906  uniioombllem5  23907  uniioombl  23909  volcn  23926  vitalilem2  23929  vitalilem5  23932  itg1lea  24032  mbfi1fseqlem6  24040  mbfi1flimlem  24042  itg2eqa  24065  itg2splitlem  24068  itg2split  24069  itg2monolem1  24070  itg2cnlem2  24082  iblabsr  24149  iblmulc2  24150  dveflem  24295  dvef  24296  dvferm2lem  24302  dvlip  24309  c1liplem1  24312  dveq0  24316  dvlt0  24321  dvivthlem1  24324  lhop1  24330  dvfsumle  24337  dvfsumlem4  24345  dvfsumrlim3  24349  dvfsum2  24350  ftc1a  24353  ftc1lem4  24355  deg1add  24416  ply1divex  24449  ply1rem  24476  fta1glem2  24479  fta1blem  24481  ig1pdvds  24489  plyeq0lem  24519  dgrcolem2  24583  plydivlem4  24604  plyrem  24613  fta1lem  24615  aalioulem3  24642  aaliou2b  24649  aaliou3lem3  24652  aaliou3lem8  24653  ulmcn  24706  ulmdvlem1  24707  itgulm  24715  pserulm  24729  pserdvlem2  24735  abelthlem2  24739  abelthlem5  24742  abelthlem6  24743  abelthlem7  24745  abelthlem8  24746  abelthlem9  24747  sinq12gt0  24812  sinq34lt0t  24814  cosq14gt0  24815  cosq14ge0  24816  efif1olem3  24845  argimgt0  24912  argimlt0  24913  logneg2  24915  logcnlem3  24944  logcnlem4  24945  logtayllem  24959  logtayl2  24962  cxpsqrtlem  25002  cxpsqrt  25003  cxpaddlelem  25049  abscxpbnd  25051  loglesqrt  25056  ang180lem2  25105  atanlogaddlem  25208  atanlogsublem  25210  atantan  25218  atans2  25226  atantayl  25232  leibpi  25238  log2tlbnd  25241  birthdaylem2  25248  birthdaylem3  25249  cxp2limlem  25271  jensenlem2  25283  jensen  25284  logdiflbnd  25290  emcllem2  25292  emcllem4  25294  harmonicbnd4  25306  fsumharmonic  25307  lgamgulmlem2  25325  lgamgulm2  25331  lgambdd  25332  lgamucov  25333  lgamcvglem  25335  lgamcvg2  25350  gamcvg  25351  wilthlem3  25365  basellem1  25376  basellem3  25378  basellem4  25379  fsumdvdsdiaglem  25478  dvdsppwf1o  25481  dvdsmulf1o  25489  chteq0  25503  chtub  25506  chpub  25514  logfacubnd  25515  logfaclbnd  25516  logexprlim  25519  perfectlem2  25524  dchrfi  25549  bclbnd  25574  bposlem1  25578  bposlem3  25580  bposlem4  25581  bposlem6  25583  lgslem1  25591  lgsqrlem2  25641  lgsqrlem4  25643  lgseisenlem2  25670  lgsquadlem1  25674  lgsquadlem2  25675  lgsquad2lem1  25678  2sqlem3  25714  2sqlem4  25715  2sqlem8  25720  2sqlem11  25723  2sqcoprm  25729  2sqmod  25730  chebbnd1lem2  25764  chebbnd1lem3  25765  chtppilimlem1  25767  chpchtlim  25773  vmadivsum  25776  vmadivsumb  25777  rpvmasumlem  25781  dchrisumlem2  25784  dchrmusum2  25788  dchrvmasumlem2  25792  dchrvmasumlem3  25793  dchrisum0flblem2  25803  dchrisum0fno1  25805  dchrisum0re  25807  dchrisum0lem1  25810  dchrisum0lem2a  25811  mudivsum  25824  mulogsumlem  25825  mulog2sumlem2  25829  vmalogdivsum2  25832  selberglem2  25840  selbergb  25843  selberg2b  25846  logdivbnd  25850  selberg3lem1  25851  selberg3lem2  25852  selberg4lem1  25854  pntrmax  25858  pntrlog2bndlem2  25872  pntrlog2bndlem3  25873  pntrlog2bndlem5  25875  pntrlog2bndlem6a  25876  pntrlog2bndlem6  25877  pntrlog2bnd  25878  pntpbnd1a  25879  pntpbnd1  25880  pntpbnd2  25881  pntibndlem1  25883  pntibndlem2  25885  pntlemb  25891  pntlemq  25895  pntlemr  25896  pntlemj  25897  pntlemk  25900  qabvle  25919  padicabvcxp  25926  ostth2lem2  25928  ostth2lem3  25929  ostth2lem4  25930  ostth3  25932  legtrid  26095  legov3  26102  krippenlem  26194  mideulem2  26238  midex  26241  opphllem5  26255  opphllem6  26256  opphl  26258  lmieu  26288  lmiisolem  26300  ttgcontlem1  26390  colinearalglem4  26414  axpaschlem  26445  axcontlem7  26475  nbfusgrlevtxm2  26879  clwlksndivn  27630  eucrct2eupthOLD  27792  eucrct2eupth  27793  nvge0  28243  smcnlem  28267  nmoub3i  28343  nmoub2i  28344  nmlno0lem  28363  minvecolem2  28446  htthlem  28489  norm3dif2  28723  bcs2  28754  chscllem2  29212  eigposi  29410  nmopub2tALT  29483  nmfnleub2  29500  nmlnop0iALT  29569  riesz1  29639  cnlnadjlem2  29642  nmopcoadji  29675  leopsq  29703  leopmul  29708  leopnmid  29712  nmopleid  29713  opsqrlem6  29719  0leopj  29760  hstle1  29800  strlem3a  29826  mdslmd4i  29907  cvexchlem  29942  cdj1i  30007  unidifsnel  30081  unidifsnne  30082  le2halvesd  30256  xlt2addrd  30259  fsumub  30315  wrdt2ind  30393  archiabllem1a  30519  archiabllem2a  30522  archiabllem2c  30523  xrge0tsmsd  30563  orngsqr  30589  ornglmulle  30590  orngrmulle  30591  orng0le1  30597  fedgmullem1  30687  fedgmullem2  30688  fzto1st1  30726  metideq  30810  metider  30811  sqsscirc1  30828  esummono  30990  esumpad2  30992  esumle  30994  esumlef  30998  esumcst  30999  esumrnmpt2  31004  esum2d  31029  aean  31181  dya2ub  31206  dya2icoseg  31213  omssubadd  31236  inelcarsg  31247  carsgsigalem  31251  carsggect  31254  carsgclctunlem2  31255  eulerpartlemb  31304  fibp1  31338  sgnmulsgp  31487  signsplypnf  31499  signsply0  31500  fdvposlt  31551  fdvposle  31553  reprgt  31573  logdivsqrle  31602  hgt750lemb  31608  hgt750leme  31610  tgoldbachgtde  31612  subfacval3  32054  sconnpht2  32103  sconnpi1  32104  resconn  32111  snmlff  32194  sinccvglem  32468  faclimlem2  32529  btwnouttr2  33037  dnibndlem5  33374  dnibndlem7  33376  dnibndlem8  33377  dnibndlem9  33378  dnibndlem10  33379  dnibnd  33383  knoppcnlem4  33388  knoppcnlem9  33393  unbdqndv2lem1  33401  unbdqndv2lem2  33402  knoppndvlem11  33414  knoppndvlem12  33415  knoppndvlem14  33417  knoppndvlem15  33418  knoppndvlem17  33420  knoppndvlem18  33421  knoppndvlem19  33422  knoppndvlem21  33424  ltflcei  34354  poimirlem9  34375  poimirlem26  34392  poimirlem27  34393  poimirlem29  34395  heicant  34401  mblfinlem2  34404  mblfinlem3  34405  mblfinlem4  34406  volsupnfl  34411  itg2addnclem  34417  itg2addnclem3  34419  iblmulc2nc  34431  bddiblnc  34436  ftc1cnnclem  34439  ftc1anclem6  34446  ftc1anclem7  34447  ftc1anclem8  34448  ftc2nc  34450  dvasin  34452  geomcau  34509  bfplem2  34576  rrncmslem  34585  rrnequiv  34588  lsatcvatlem  35663  islshpcv  35667  atlatmstc  35933  cvlsupr7  35962  cvrval3  36027  cvrval5  36029  cvrexchlem  36033  atcvrj1  36045  cvrat3  36056  cvrat4  36057  atbtwn  36060  1cvratex  36087  hlatexch4  36095  3atlem1  36097  3atlem2  36098  atcvrlln2  36133  atcvrlln  36134  lplnllnneN  36170  llncvrlpln2  36171  4atlem3b  36212  lplncvrlvol2  36229  dalemswapyz  36270  dalemswapyzps  36304  dalem25  36312  dalem39  36325  dalem58  36344  dalem59  36345  lneq2at  36392  lncvrat  36396  dalawlem2  36486  dalawlem3  36487  dalawlem4  36488  dalawlem6  36490  dalawlem9  36493  dalawlem11  36495  dalawlem12  36496  lhpocnle  36630  lhpmcvr3  36639  lhpmcvr5N  36641  lhpmcvr6N  36642  4atexlemunv  36680  4atexlemc  36683  4atexlemex2  36685  lautm  36708  cdlemc2  36806  cdleme5  36854  cdleme11j  36881  cdleme16b  36893  cdlemednpq  36913  cdleme19e  36921  cdleme20i  36931  cdleme22a  36954  cdleme22cN  36956  cdleme22d  36957  cdleme22e  36958  cdleme22eALTN  36959  cdleme22f  36960  cdleme23c  36965  cdleme30a  36992  cdleme35a  37062  cdleme35b  37064  cdleme42h  37096  cdlemeg46rgv  37142  cdlemg8b  37242  cdlemg12e  37261  cdlemg13a  37265  cdlemg17pq  37286  cdlemg18c  37294  cdlemg19  37298  cdlemg21  37300  cdlemg31d  37314  cdlemg33a  37320  tendoid  37387  cdlemk4  37448  cdlemki  37455  cdlemk10  37457  cdlemksv2  37461  cdlemk12  37464  cdlemk14  37468  cdlemk15  37469  cdlemk1u  37473  cdlemk5u  37475  cdlemk12u  37486  cdlemk45  37561  cdlemk48  37564  dia2dimlem1  37678  dia2dimlem2  37679  dia2dimlem3  37680  cdlemm10N  37732  cdlemn2  37809  dihjustlem  37830  dihglbcpreN  37914  dihmeetlem3N  37919  zrtdvds  38659  rtprmirr  38660  dffltz  38712  fltnlta  38716  irrapxlem1  38849  pell1qrgaplem  38900  pell1qrgap  38901  monotoddzzfi  38969  jm2.24nn  38986  congtr  38992  congmul  38994  congsub  38997  fzmaxdif  39008  acongeq  39010  jm2.20nn  39024  jm2.25  39026  hbtlem4  39156  dgrsub2  39165  mpaaeu  39180  idomsubgmo  39228  leeq2d  39905  int-sqgeq0d  39938  int-ineqmvtd  39943  cvgdvgrat  40095  radcnvrat  40096  hashnzfzclim  40104  dvconstbi  40116  binomcxplemdvbinom  40135  isosctrlem1ALT  40721  mulltgt0  40732  rnmptbd2lem  40978  oddfl  41002  2timesgt  41013  lt3addmuld  41027  lt4addmuld  41032  supxrgere  41060  supxrgelem  41064  supxrge  41065  xadd0ge2  41068  infrpge  41078  xrlexaddrp  41079  xralrple2  41081  infxr  41094  infleinflem1  41097  infleinflem2  41098  infleinf  41099  xralrple4  41100  xralrple3  41101  recnnltrp  41104  rpgtrecnn  41108  xrralrecnnge  41122  rexabslelem  41153  infrnmptle  41158  supminfxr  41201  xrpnf  41223  iccshift  41255  iooshift  41259  ressiocsup  41291  ressioosup  41292  fsumnncl  41313  fmul01  41322  fmul01lt1lem1  41326  fmul01lt1lem2  41327  mccllem  41339  climrec  41345  climexp  41347  climneg  41352  limcrecl  41371  sumnnodd  41372  lptioo2  41373  lptioo1  41374  ltmod  41380  lptre2pt  41382  0ellimcdiv  41391  limclner  41393  fnlimcnv  41409  climinf2lem  41448  limsupubuzlem  41454  limsup10exlem  41514  limsupgtlem  41519  dfxlim2v  41589  xlimliminflimsup  41604  cncficcgt0  41631  cncfioobdlem  41639  ioodvbdlimc1lem1  41676  ioodvbdlimc1lem2  41677  ioodvbdlimc2lem  41679  dvdsn1add  41684  dvnxpaek  41687  dvnmul  41688  dvnprodlem1  41691  itgiccshift  41725  itgperiod  41726  sublevolico  41730  ismbl3  41732  ovolsplit  41734  ismbl4  41739  stoweidlem1  41747  stoweidlem11  41757  stoweidlem13  41759  stoweidlem26  41772  stoweidlem34  41780  stoweidlem38  41784  stoweidlem42  41788  stoweidlem51  41797  stoweidlem59  41805  stirlinglem5  41824  stirlinglem6  41825  stirlinglem7  41826  stirlinglem10  41829  stirlinglem11  41830  stirlinglem13  41832  stirlinglem15  41834  dirkercncflem1  41849  dirkercncflem4  41852  fourierdlem4  41857  fourierdlem10  41863  fourierdlem11  41864  fourierdlem15  41868  fourierdlem20  41873  fourierdlem25  41878  fourierdlem26  41879  fourierdlem30  41883  fourierdlem37  41890  fourierdlem39  41892  fourierdlem40  41893  fourierdlem41  41894  fourierdlem42  41895  fourierdlem44  41897  fourierdlem47  41899  fourierdlem48  41900  fourierdlem49  41901  fourierdlem50  41902  fourierdlem51  41903  fourierdlem52  41904  fourierdlem54  41906  fourierdlem60  41912  fourierdlem61  41913  fourierdlem63  41915  fourierdlem64  41916  fourierdlem65  41917  fourierdlem73  41925  fourierdlem74  41926  fourierdlem75  41927  fourierdlem76  41928  fourierdlem78  41930  fourierdlem79  41931  fourierdlem81  41933  fourierdlem84  41936  fourierdlem87  41939  fourierdlem92  41944  fourierdlem93  41945  fourierdlem101  41953  fourierdlem102  41954  fourierdlem103  41955  fourierdlem104  41956  fourierdlem111  41963  fourierdlem114  41966  sqwvfoura  41974  sqwvfourb  41975  fouriersw  41977  etransclem19  41999  etransclem23  42003  etransclem24  42004  etransclem25  42005  etransclem27  42007  etransclem32  42012  etransclem35  42015  etransclem48  42028  qndenserrnbllem  42040  ioorrnopnlem  42050  ioorrnopnxrlem  42052  fsumlesge0  42120  sge0cl  42124  sge0supre  42132  sge0less  42135  sge0gerp  42138  sge0ltfirp  42143  sge0le  42150  sge0ltfirpmpt  42151  sge0split  42152  sge0rpcpnf  42164  sge0ltfirpmpt2  42169  sge0isum  42170  sge0xaddlem1  42176  sge0pnffigtmpt  42183  sge0pnffsumgt  42185  sge0gtfsumgt  42186  sge0seq  42189  nnfoctbdjlem  42198  meassle  42206  meaiuninclem  42223  meaiininclem  42229  omeiunle  42260  omeiunltfirp  42262  carageniuncllem2  42265  carageniuncl  42266  omess0  42277  hoicvr  42291  ovnlerp  42305  ovnsubaddlem1  42313  hsphoidmvle2  42328  hoidmv1lelem2  42335  hoidmv1le  42337  hoidmvlelem1  42338  hoidmvlelem2  42339  hoidmvlelem3  42340  hoidmvlelem5  42342  ovnhoilem2  42345  ovnhoi  42346  hoidifhspdmvle  42363  hoiqssbllem2  42366  hspmbllem2  42370  hspmbllem3  42371  hspmbl  42372  vonioolem2  42424  vonicclem2  42427  smfaddlem1  42500  smflimlem2  42509  smflimlem4  42511  smfmullem1  42527  smfinflem  42552  smflimsuplem4  42558  smflimsuplem8  42562  perfectALTVlem2  43285  nnpw2blen  44038  itscnhlinecirc02plem1  44167