Theorem breqtrd 5092

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

Syntax hints:   → wi 4   = wceq 1537   class class class wbr 5066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067

This theorem is referenced by:  breqtrrd  5094  breqtrid  5103  domunsn  8667  mapdom2  8688  phplem4  8699  mapfien2  8872  wemaplem2  9011  infdifsn  9120  cantnff  9137  infxpenlem  9439  infmap2  9640  ssfin4  9732  canthp1lem1  10074  nqereq  10357  ltexnq  10397  ltbtwnnq  10400  add20  11152  mullt0  11159  ltm1  11482  recgt0  11486  prodgt0  11487  ltmul1a  11489  mulge0b  11510  recp1lt1  11538  recreclt  11539  ledivp1  11542  ledivp1i  11565  ltdivp1i  11566  eluzmn  12251  ltaddrp2d  12466  mul2lt0bi  12496  prodge0rd  12497  xleadd1a  12647  xov1plusxeqvd  12885  fz01en  12936  fzonmapblen  13084  fladdz  13196  flhalf  13201  fldiv  13229  modsubdir  13309  fzen2  13338  serle  13426  ltexp2a  13531  leexp2a  13537  exple1  13541  expubnd  13542  bernneq  13591  expmulnbnd  13597  discr1  13601  discr  13602  faclbnd6  13660  hashfz  13789  hashfun  13799  seqcoll  13823  sqeqd  14525  sqrlem7  14608  sqrtge0  14617  sqrtneglem  14626  abslt  14674  absle  14675  abstri  14690  rlimge0  14938  reccn2  14953  climaddc2  14992  isercolllem1  15021  caucvgrlem  15029  summolem2a  15072  isumge0  15121  fsumle  15154  fsumlt  15155  o1fsum  15168  supcvg  15211  expcnv  15219  geolim  15226  geolim2  15227  georeclim  15228  geo2lim  15231  mertenslem1  15240  mertens  15242  prodmolem2a  15288  efcllem  15431  ef0lem  15432  efgt0  15456  eftlub  15462  eflt  15470  sinbnd  15533  cosbnd  15534  ef01bndlem  15537  sin01gt0  15543  cos01gt0  15544  sin02gt0  15545  eirrlem  15557  rpnnen2lem11  15577  rpnnen2lem12  15578  ruclem11  15593  dvdssub2  15651  dvdsadd2b  15656  dvdsexp  15677  3dvds  15680  opoe  15712  bitsfzolem  15783  bitsinv1lem  15790  bezoutlem4  15890  dvdsgcd  15892  dvdsmulgcd  15905  bezoutr1  15913  nn0seqcvgd  15914  rpmulgcd2  16000  qredeq  16001  rpdvds  16004  prmind2  16029  divdenle  16089  hashdvds  16112  phimullem  16116  eulerthlem2  16119  prmdiveq  16123  prmdivdiv  16124  pythagtriplem4  16156  pythagtriplem10  16157  pythagtriplem19  16170  iserodd  16172  pcpre1  16179  pcadd2  16226  qexpz  16237  expnprm  16238  oddprmdvds  16239  pockthlem  16241  prmreclem2  16253  prmreclem3  16254  4sqlem7  16280  4sqlem10  16283  4sqlem11  16291  4sqlem12  16292  4sqlem14  16294  4sqlem15  16295  4sqlem16  16296  0ram  16356  ffthiso  17199  latmlej12  17701  qusgrp  18335  pgpfi1  18720  sylow1lem4  18726  sylow1lem5  18727  odcau  18729  pgpfi  18730  pgpssslw  18739  sylow3lem4  18755  sylow3lem6  18757  efgsfo  18865  frgp0  18886  odadd1  18968  odadd2  18969  odadd  18970  gexexlem  18972  lt6abl  19015  gsumzsubmcl  19038  pwsgsum  19102  dprd2dlem1  19163  dprd2d2  19166  ablfacrplem  19187  ablfacrp  19188  ablfacrp2  19189  ablfac1b  19192  ablfac1eu  19195  pgpfac1lem3a  19198  ablfaclem2  19208  dvdsrid  19401  dvdsrtr  19402  dvdsrneg  19404  unitmulcl  19414  unitgrp  19417  unitnegcl  19431  isdrng2  19512  subrguss  19550  subrgunit  19553  abvsubtri  19606  fidomndrnglem  20079  psrbaglesupp  20148  gzrngunit  20611  prmirredlem  20640  znidomb  20708  frlmgsum  20916  invrvald  21285  psmetsym  22920  psmettri  22921  mettri2  22951  xmetsym  22957  xmettri  22961  prdsxmetlem  22978  xblss2ps  23011  xblss2  23012  blhalf  23015  xmsge0  23073  ngptgp  23245  nrginvrcnlem  23300  nmoeq0  23345  cnmet  23380  blcvx  23406  opnreen  23439  metdcnlem  23444  metdstri  23459  metdsle  23460  metnrmlem1  23467  metnrmlem3  23469  lebnumlem1  23565  pi1inv  23656  cphnmf  23799  ipge0  23802  ipcau2  23837  tcphcphlem1  23838  csbren  24002  minveclem2  24029  minveclem3  24032  ovolssnul  24088  ovolctb  24091  ovolunnul  24101  ovoliunlem1  24103  ovoliun2  24107  ovoliunnul  24108  ioombl1lem4  24162  uniioombllem3  24186  uniioombllem4  24187  uniioombllem5  24188  uniioombl  24190  volcn  24207  vitalilem2  24210  vitalilem5  24213  itg1lea  24313  mbfi1fseqlem6  24321  mbfi1flimlem  24323  itg2eqa  24346  itg2splitlem  24349  itg2split  24350  itg2monolem1  24351  itg2cnlem2  24363  iblabsr  24430  iblmulc2  24431  dveflem  24576  dvef  24577  dvferm2lem  24583  dvlip  24590  c1liplem1  24593  dveq0  24597  dvlt0  24602  dvivthlem1  24605  lhop1  24611  dvfsumle  24618  dvfsumlem4  24626  dvfsumrlim3  24630  dvfsum2  24631  ftc1a  24634  ftc1lem4  24636  deg1add  24697  ply1divex  24730  ply1rem  24757  fta1glem2  24760  fta1blem  24762  ig1pdvds  24770  plyeq0lem  24800  dgrcolem2  24864  plydivlem4  24885  plyrem  24894  fta1lem  24896  aalioulem3  24923  aaliou2b  24930  aaliou3lem3  24933  aaliou3lem8  24934  ulmcn  24987  ulmdvlem1  24988  itgulm  24996  pserulm  25010  pserdvlem2  25016  abelthlem2  25020  abelthlem5  25023  abelthlem6  25024  abelthlem7  25026  abelthlem8  25027  abelthlem9  25028  sinq12gt0  25093  sinq34lt0t  25095  cosq14gt0  25096  cosq14ge0  25097  cos02pilt1  25111  efif1olem3  25128  argimgt0  25195  argimlt0  25196  logneg2  25198  logcnlem3  25227  logcnlem4  25228  logtayllem  25242  logtayl2  25245  cxpsqrtlem  25285  cxpsqrt  25286  cxpaddlelem  25332  abscxpbnd  25334  loglesqrt  25339  ang180lem2  25388  atanlogaddlem  25491  atanlogsublem  25493  atantan  25501  atans2  25509  atantayl  25515  leibpi  25520  log2tlbnd  25523  birthdaylem2  25530  birthdaylem3  25531  cxp2limlem  25553  jensenlem2  25565  jensen  25566  logdiflbnd  25572  emcllem2  25574  emcllem4  25576  harmonicbnd4  25588  fsumharmonic  25589  lgamgulmlem2  25607  lgamgulm2  25613  lgambdd  25614  lgamucov  25615  lgamcvglem  25617  lgamcvg2  25632  gamcvg  25633  wilthlem3  25647  basellem1  25658  basellem3  25660  basellem4  25661  fsumdvdsdiaglem  25760  dvdsppwf1o  25763  dvdsmulf1o  25771  chteq0  25785  chtub  25788  chpub  25796  logfacubnd  25797  logfaclbnd  25798  logexprlim  25801  perfectlem2  25806  dchrfi  25831  bclbnd  25856  bposlem1  25860  bposlem3  25862  bposlem4  25863  bposlem6  25865  lgslem1  25873  lgsqrlem2  25923  lgsqrlem4  25925  lgseisenlem2  25952  lgsquadlem1  25956  lgsquadlem2  25957  lgsquad2lem1  25960  2sqlem3  25996  2sqlem4  25997  2sqlem8  26002  2sqlem11  26005  2sqcoprm  26011  2sqmod  26012  chebbnd1lem2  26046  chebbnd1lem3  26047  chtppilimlem1  26049  chpchtlim  26055  vmadivsum  26058  vmadivsumb  26059  rpvmasumlem  26063  dchrisumlem2  26066  dchrmusum2  26070  dchrvmasumlem2  26074  dchrvmasumlem3  26075  dchrisum0flblem2  26085  dchrisum0fno1  26087  dchrisum0re  26089  dchrisum0lem1  26092  dchrisum0lem2a  26093  mudivsum  26106  mulogsumlem  26107  mulog2sumlem2  26111  vmalogdivsum2  26114  selberglem2  26122  selbergb  26125  selberg2b  26128  logdivbnd  26132  selberg3lem1  26133  selberg3lem2  26134  selberg4lem1  26136  pntrmax  26140  pntrlog2bndlem2  26154  pntrlog2bndlem3  26155  pntrlog2bndlem5  26157  pntrlog2bndlem6a  26158  pntrlog2bndlem6  26159  pntrlog2bnd  26160  pntpbnd1a  26161  pntpbnd1  26162  pntpbnd2  26163  pntibndlem1  26165  pntibndlem2  26167  pntlemb  26173  pntlemq  26177  pntlemr  26178  pntlemj  26179  pntlemk  26182  qabvle  26201  padicabvcxp  26208  ostth2lem2  26210  ostth2lem3  26211  ostth2lem4  26212  ostth3  26214  legtrid  26377  legov3  26384  krippenlem  26476  mideulem2  26520  midex  26523  opphllem5  26537  opphllem6  26538  opphl  26540  lmieu  26570  lmiisolem  26582  ttgcontlem1  26671  colinearalglem4  26695  axpaschlem  26726  axcontlem7  26756  nbfusgrlevtxm2  27160  clwlksndivn  27865  eucrct2eupth  28024  nvge0  28450  smcnlem  28474  nmoub3i  28550  nmoub2i  28551  nmlno0lem  28570  minvecolem2  28652  htthlem  28694  norm3dif2  28928  bcs2  28959  chscllem2  29415  eigposi  29613  nmopub2tALT  29686  nmfnleub2  29703  nmlnop0iALT  29772  riesz1  29842  cnlnadjlem2  29845  nmopcoadji  29878  leopsq  29906  leopmul  29911  leopnmid  29915  nmopleid  29916  opsqrlem6  29922  0leopj  29963  hstle1  30003  strlem3a  30029  mdslmd4i  30110  cvexchlem  30145  cdj1i  30210  unidifsnel  30295  unidifsnne  30296  le2halvesd  30479  xlt2addrd  30482  fsumub  30544  wrdt2ind  30627  xrge0tsmsd  30692  fzto1st1  30744  cycpmco2lem4  30771  cycpmco2lem6  30773  cyc3conja  30799  archiabllem1a  30820  archiabllem2a  30823  archiabllem2c  30824  orngsqr  30877  ornglmulle  30878  orngrmulle  30879  orng0le1  30885  fedgmullem1  31025  fedgmullem2  31026  metideq  31133  metider  31134  sqsscirc1  31151  esummono  31313  esumpad2  31315  esumle  31317  esumlef  31321  esumcst  31322  esumrnmpt2  31327  esum2d  31352  aean  31503  dya2ub  31528  dya2icoseg  31535  omssubadd  31558  inelcarsg  31569  carsgsigalem  31573  carsggect  31576  carsgclctunlem2  31577  eulerpartlemb  31626  fibp1  31659  sgnmulsgp  31808  signsplypnf  31820  signsply0  31821  fdvposlt  31870  fdvposle  31872  reprgt  31892  logdivsqrle  31921  hgt750lemb  31927  hgt750leme  31929  tgoldbachgtde  31931  subfacval3  32436  sconnpht2  32485  sconnpi1  32486  resconn  32493  snmlff  32576  sinccvglem  32915  faclimlem2  32976  btwnouttr2  33483  dnibndlem5  33821  dnibndlem7  33823  dnibndlem8  33824  dnibndlem9  33825  dnibndlem10  33826  dnibnd  33830  knoppcnlem4  33835  knoppcnlem9  33840  unbdqndv2lem1  33848  unbdqndv2lem2  33849  knoppndvlem11  33861  knoppndvlem12  33862  knoppndvlem14  33864  knoppndvlem15  33865  knoppndvlem17  33867  knoppndvlem18  33868  knoppndvlem19  33869  knoppndvlem21  33871  ltflcei  34895  poimirlem9  34916  poimirlem26  34933  poimirlem27  34934  poimirlem29  34936  heicant  34942  mblfinlem2  34945  mblfinlem3  34946  mblfinlem4  34947  volsupnfl  34952  itg2addnclem  34958  itg2addnclem3  34960  iblmulc2nc  34972  bddiblnc  34977  ftc1cnnclem  34980  ftc1anclem6  34987  ftc1anclem7  34988  ftc1anclem8  34989  ftc2nc  34991  dvasin  34993  geomcau  35049  bfplem2  35116  rrncmslem  35125  rrnequiv  35128  lsatcvatlem  36200  islshpcv  36204  atlatmstc  36470  cvlsupr7  36499  cvrval3  36564  cvrval5  36566  cvrexchlem  36570  atcvrj1  36582  cvrat3  36593  cvrat4  36594  atbtwn  36597  1cvratex  36624  hlatexch4  36632  3atlem1  36634  3atlem2  36635  atcvrlln2  36670  atcvrlln  36671  lplnllnneN  36707  llncvrlpln2  36708  4atlem3b  36749  lplncvrlvol2  36766  dalemswapyz  36807  dalemswapyzps  36841  dalem25  36849  dalem39  36862  dalem58  36881  dalem59  36882  lneq2at  36929  lncvrat  36933  dalawlem2  37023  dalawlem3  37024  dalawlem4  37025  dalawlem6  37027  dalawlem9  37030  dalawlem11  37032  dalawlem12  37033  lhpocnle  37167  lhpmcvr3  37176  lhpmcvr5N  37178  lhpmcvr6N  37179  4atexlemunv  37217  4atexlemc  37220  4atexlemex2  37222  lautm  37245  cdlemc2  37343  cdleme5  37391  cdleme11j  37418  cdleme16b  37430  cdlemednpq  37450  cdleme19e  37458  cdleme20i  37468  cdleme22a  37491  cdleme22cN  37493  cdleme22d  37494  cdleme22e  37495  cdleme22eALTN  37496  cdleme22f  37497  cdleme23c  37502  cdleme30a  37529  cdleme35a  37599  cdleme35b  37601  cdleme42h  37633  cdlemeg46rgv  37679  cdlemg8b  37779  cdlemg12e  37798  cdlemg13a  37802  cdlemg17pq  37823  cdlemg18c  37831  cdlemg19  37835  cdlemg21  37837  cdlemg31d  37851  cdlemg33a  37857  tendoid  37924  cdlemk4  37985  cdlemki  37992  cdlemk10  37994  cdlemksv2  37998  cdlemk12  38001  cdlemk14  38005  cdlemk15  38006  cdlemk1u  38010  cdlemk5u  38012  cdlemk12u  38023  cdlemk45  38098  cdlemk48  38101  dia2dimlem1  38215  dia2dimlem2  38216  dia2dimlem3  38217  cdlemm10N  38269  cdlemn2  38346  dihjustlem  38367  dihglbcpreN  38451  dihmeetlem3N  38456  2xp3dxp2ge1d  39146  factwoffsmonot  39147  zrtdvds  39242  rtprmirr  39243  dffltz  39320  fltnlta  39324  irrapxlem1  39468  pell1qrgaplem  39519  pell1qrgap  39520  monotoddzzfi  39588  jm2.24nn  39605  congtr  39611  congmul  39613  congsub  39616  fzmaxdif  39627  acongeq  39629  jm2.20nn  39643  jm2.25  39645  hbtlem4  39775  dgrsub2  39784  mpaaeu  39799  idomsubgmo  39847  iscard4  39949  leeq2d  40557  int-sqgeq0d  40588  int-ineqmvtd  40593  cvgdvgrat  40694  radcnvrat  40695  hashnzfzclim  40703  dvconstbi  40715  binomcxplemdvbinom  40734  isosctrlem1ALT  41317  mulltgt0  41328  rnmptbd2lem  41569  oddfl  41592  2timesgt  41603  lt3addmuld  41617  lt4addmuld  41622  supxrgere  41650  supxrgelem  41654  supxrge  41655  xadd0ge2  41658  infrpge  41668  xrlexaddrp  41669  xralrple2  41671  infxr  41684  infleinflem1  41687  infleinflem2  41688  infleinf  41689  xralrple4  41690  xralrple3  41691  recnnltrp  41694  rpgtrecnn  41698  xrralrecnnge  41711  rexabslelem  41741  infrnmptle  41746  supminfxr  41789  xrpnf  41811  iccshift  41843  iooshift  41847  ressiocsup  41879  ressioosup  41880  fsumnncl  41901  fmul01  41910  fmul01lt1lem1  41914  fmul01lt1lem2  41915  mccllem  41927  climrec  41933  climexp  41935  climneg  41940  limcrecl  41959  sumnnodd  41960  lptioo2  41961  lptioo1  41962  ltmod  41968  lptre2pt  41970  0ellimcdiv  41979  limclner  41981  fnlimcnv  41997  climinf2lem  42036  limsupubuzlem  42042  limsup10exlem  42102  limsupgtlem  42107  dfxlim2v  42177  xlimliminflimsup  42192  cncficcgt0  42220  cncfioobdlem  42228  ioodvbdlimc1lem1  42265  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  dvdsn1add  42273  dvnxpaek  42276  dvnmul  42277  dvnprodlem1  42280  itgiccshift  42314  itgperiod  42315  sublevolico  42318  ismbl3  42320  ovolsplit  42322  ismbl4  42327  stoweidlem1  42335  stoweidlem11  42345  stoweidlem13  42347  stoweidlem26  42360  stoweidlem34  42368  stoweidlem38  42372  stoweidlem42  42376  stoweidlem51  42385  stoweidlem59  42393  stirlinglem5  42412  stirlinglem6  42413  stirlinglem7  42414  stirlinglem10  42417  stirlinglem11  42418  stirlinglem13  42420  stirlinglem15  42422  dirkercncflem1  42437  dirkercncflem4  42440  fourierdlem4  42445  fourierdlem10  42451  fourierdlem11  42452  fourierdlem15  42456  fourierdlem20  42461  fourierdlem25  42466  fourierdlem26  42467  fourierdlem30  42471  fourierdlem37  42478  fourierdlem39  42480  fourierdlem40  42481  fourierdlem41  42482  fourierdlem42  42483  fourierdlem44  42485  fourierdlem47  42487  fourierdlem48  42488  fourierdlem49  42489  fourierdlem50  42490  fourierdlem51  42491  fourierdlem52  42492  fourierdlem54  42494  fourierdlem60  42500  fourierdlem61  42501  fourierdlem63  42503  fourierdlem64  42504  fourierdlem65  42505  fourierdlem73  42513  fourierdlem74  42514  fourierdlem75  42515  fourierdlem76  42516  fourierdlem78  42518  fourierdlem79  42519  fourierdlem81  42521  fourierdlem84  42524  fourierdlem87  42527  fourierdlem92  42532  fourierdlem93  42533  fourierdlem101  42541  fourierdlem102  42542  fourierdlem103  42543  fourierdlem104  42544  fourierdlem111  42551  fourierdlem114  42554  sqwvfoura  42562  sqwvfourb  42563  fouriersw  42565  etransclem19  42587  etransclem23  42591  etransclem24  42592  etransclem25  42593  etransclem27  42595  etransclem32  42600  etransclem35  42603  etransclem48  42616  qndenserrnbllem  42628  ioorrnopnlem  42638  ioorrnopnxrlem  42640  fsumlesge0  42708  sge0cl  42712  sge0supre  42720  sge0less  42723  sge0gerp  42726  sge0ltfirp  42731  sge0le  42738  sge0ltfirpmpt  42739  sge0split  42740  sge0rpcpnf  42752  sge0ltfirpmpt2  42757  sge0isum  42758  sge0xaddlem1  42764  sge0pnffigtmpt  42771  sge0pnffsumgt  42773  sge0gtfsumgt  42774  sge0seq  42777  nnfoctbdjlem  42786  meassle  42794  meaiuninclem  42811  meaiininclem  42817  omeiunle  42848  omeiunltfirp  42850  carageniuncllem2  42853  carageniuncl  42854  omess0  42865  hoicvr  42879  ovnlerp  42893  ovnsubaddlem1  42901  hsphoidmvle2  42916  hoidmv1lelem2  42923  hoidmv1le  42925  hoidmvlelem1  42926  hoidmvlelem2  42927  hoidmvlelem3  42928  hoidmvlelem5  42930  ovnhoilem2  42933  ovnhoi  42934  hoidifhspdmvle  42951  hoiqssbllem2  42954  hspmbllem2  42958  hspmbllem3  42959  hspmbl  42960  vonioolem2  43012  vonicclem2  43015  smfaddlem1  43088  smflimlem2  43097  smflimlem4  43099  smfmullem1  43115  smfinflem  43140  smflimsuplem4  43146  smflimsuplem8  43150  perfectALTVlem2  43936  nnpw2blen  44689  itscnhlinecirc02plem1  44818