Theorem breqtrd 5168

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

Syntax hints:   → wi 4   = wceq 1534   class class class wbr 5142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-br 5143

This theorem is referenced by:  breqtrrd  5170  breqtrid  5179  domunsn  9143  mapdom2  9164  phplem2  9224  phplem4OLD  9236  mapfien2  9424  wemaplem2  9562  infdifsn  9672  cantnff  9689  ttrclss  9735  rnttrcl  9737  infxpenlem  10028  infmap2  10233  ssfin4  10325  canthp1lem1  10667  nqereq  10950  ltexnq  10990  ltbtwnnq  10993  add20  11748  mullt0  11755  ltm1  12078  recgt0  12082  prodgt0  12083  ltmul1a  12085  mulge0b  12106  recp1lt1  12134  recreclt  12135  ledivp1  12138  ledivp1i  12161  ltdivp1i  12162  eluzmn  12851  ltaddrp2d  13074  mul2lt0bi  13104  prodge0rd  13105  xleadd1a  13256  xov1plusxeqvd  13499  fz01en  13553  fzonmapblen  13702  fladdz  13814  flhalf  13819  fldiv  13849  modsubdir  13929  fzen2  13958  serle  14046  ltexp2a  14154  leexp2a  14160  exple1  14164  expubnd  14165  bernneq  14215  expmulnbnd  14221  discr1  14225  discr  14226  faclbnd6  14282  hashfz  14410  hashfun  14420  seqcoll  14449  sqeqd  15137  01sqrexlem7  15219  sqrtge0  15228  sqrtneglem  15237  abslt  15285  absle  15286  abstri  15301  rlimge0  15549  reccn2  15565  climaddc2  15604  isercolllem1  15635  caucvgrlem  15643  summolem2a  15685  isumge0  15736  fsumle  15769  fsumlt  15770  o1fsum  15783  supcvg  15826  expcnv  15834  geolim  15840  geolim2  15841  georeclim  15842  geo2lim  15845  mertenslem1  15854  mertens  15856  prodmolem2a  15902  efcllem  16045  ef0lem  16046  efgt0  16071  eftlub  16077  eflt  16085  sinbnd  16148  cosbnd  16149  ef01bndlem  16152  sin01gt0  16158  cos01gt0  16159  sin02gt0  16160  eirrlem  16172  rpnnen2lem11  16192  rpnnen2lem12  16193  ruclem11  16208  dvdssub2  16269  dvdsadd2b  16274  dvdsexp  16296  3dvds  16299  opoe  16331  bitsfzolem  16400  bitsinv1lem  16407  bezoutlem4  16509  dvdsgcd  16511  dvdsmulgcd  16522  bezoutr1  16531  nn0seqcvgd  16532  rpmulgcd2  16618  qredeq  16619  rpdvds  16622  prmind2  16647  divdenle  16712  hashdvds  16735  phimullem  16739  eulerthlem2  16742  prmdiveq  16746  prmdivdiv  16747  pythagtriplem4  16779  pythagtriplem10  16780  pythagtriplem19  16793  iserodd  16795  pcpre1  16802  pcadd2  16850  qexpz  16861  expnprm  16862  oddprmdvds  16863  pockthlem  16865  prmreclem2  16877  prmreclem3  16878  4sqlem7  16904  4sqlem10  16907  4sqlem11  16915  4sqlem12  16916  4sqlem14  16918  4sqlem15  16919  4sqlem16  16920  0ram  16980  ffthiso  17909  latmlej12  18462  qusgrp  19132  pgpfi1  19541  sylow1lem4  19547  sylow1lem5  19548  odcau  19550  pgpfi  19551  pgpssslw  19560  sylow3lem4  19576  sylow3lem6  19578  efgsfo  19685  frgp0  19706  odadd1  19794  odadd2  19795  odadd  19796  gexexlem  19798  lt6abl  19841  gsumzsubmcl  19864  pwsgsum  19928  dprd2dlem1  19989  dprd2d2  19992  ablfacrplem  20013  ablfacrp  20014  ablfacrp2  20015  ablfac1b  20018  ablfac1eu  20021  pgpfac1lem3a  20024  ablfaclem2  20034  dvdsrid  20295  dvdsrtr  20296  dvdsrneg  20298  unitmulcl  20308  unitgrp  20311  unitnegcl  20325  subrguss  20515  subrgunit  20518  isdrng2  20627  abvsubtri  20704  fidomndrnglem  21247  gzrngunit  21353  prmirredlem  21385  znidomb  21482  frlmgsum  21693  psrbaglesupp  21844  psrbaglesuppOLD  21845  psdmul  22077  invrvald  22565  psmetsym  24203  psmettri  24204  mettri2  24234  xmetsym  24240  xmettri  24244  prdsxmetlem  24261  xblss2ps  24294  xblss2  24295  blhalf  24298  xmsge0  24356  ngptgp  24532  nrginvrcnlem  24595  nmoeq0  24640  cnmet  24675  blcvx  24701  opnreen  24734  metdcnlem  24739  metdstri  24754  metdsle  24755  metnrmlem1  24762  metnrmlem3  24764  lebnumlem1  24874  pi1inv  24966  cphnmf  25110  ipge0  25113  ipcau2  25149  tcphcphlem1  25150  csbren  25314  minveclem2  25341  minveclem3  25344  ovolssnul  25403  ovolctb  25406  ovolunnul  25416  ovoliunlem1  25418  ovoliun2  25422  ovoliunnul  25423  ioombl1lem4  25477  uniioombllem3  25501  uniioombllem4  25502  uniioombllem5  25503  uniioombl  25505  volcn  25522  vitalilem2  25525  vitalilem5  25528  itg1lea  25629  mbfi1fseqlem6  25637  mbfi1flimlem  25639  itg2eqa  25662  itg2splitlem  25665  itg2split  25666  itg2monolem1  25667  itg2cnlem2  25679  iblabsr  25746  iblmulc2  25747  bddiblnc  25758  dveflem  25898  dvef  25899  dvferm2lem  25905  dvlip  25913  c1liplem1  25916  dveq0  25920  dvlt0  25925  dvivthlem1  25928  lhop1  25934  dvfsumle  25941  dvfsumleOLD  25942  dvfsumlem4  25951  dvfsumrlim3  25955  dvfsum2  25956  ftc1a  25959  ftc1lem4  25961  deg1add  26026  ply1divex  26059  ply1rem  26087  fta1glem2  26090  fta1blem  26092  ig1pdvds  26101  plyeq0lem  26131  dgrcolem2  26196  plydivlem4  26218  plyrem  26227  fta1lem  26229  aalioulem3  26256  aaliou2b  26263  aaliou3lem3  26266  aaliou3lem8  26267  ulmcn  26322  ulmdvlem1  26323  itgulm  26331  pserulm  26345  pserdvlem2  26352  abelthlem2  26356  abelthlem5  26359  abelthlem6  26360  abelthlem7  26362  abelthlem8  26363  abelthlem9  26364  sinq12gt0  26429  sinq34lt0t  26431  cosq14gt0  26432  cosq14ge0  26433  cos02pilt1  26447  efif1olem3  26465  argimgt0  26533  argimlt0  26534  logneg2  26536  logcnlem3  26565  logcnlem4  26566  logtayllem  26580  logtayl2  26583  cxpsqrtlem  26623  cxpsqrt  26624  cxpaddlelem  26673  abscxpbnd  26675  loglesqrt  26680  ang180lem2  26729  atanlogaddlem  26832  atanlogsublem  26834  atantan  26842  atans2  26850  atantayl  26856  leibpi  26861  log2tlbnd  26864  birthdaylem2  26871  birthdaylem3  26872  cxp2limlem  26895  jensenlem2  26907  jensen  26908  logdiflbnd  26914  emcllem2  26916  emcllem4  26918  harmonicbnd4  26930  fsumharmonic  26931  lgamgulmlem2  26949  lgamgulm2  26955  lgambdd  26956  lgamucov  26957  lgamcvglem  26959  lgamcvg2  26974  gamcvg  26975  wilthlem3  26989  basellem1  27000  basellem3  27002  basellem4  27003  fsumdvdsdiaglem  27102  dvdsppwf1o  27105  mpodvdsmulf1o  27113  dvdsmulf1o  27115  chteq0  27129  chtub  27132  chpub  27140  logfacubnd  27141  logfaclbnd  27142  logexprlim  27145  perfectlem2  27150  dchrfi  27175  bclbnd  27200  bposlem1  27204  bposlem3  27206  bposlem4  27207  bposlem6  27209  lgslem1  27217  lgsqrlem2  27267  lgsqrlem4  27269  lgseisenlem2  27296  lgsquadlem1  27300  lgsquadlem2  27301  lgsquad2lem1  27304  2sqlem3  27340  2sqlem4  27341  2sqlem8  27346  2sqlem11  27349  2sqcoprm  27355  2sqmod  27356  chebbnd1lem2  27390  chebbnd1lem3  27391  chtppilimlem1  27393  chpchtlim  27399  vmadivsum  27402  vmadivsumb  27403  rpvmasumlem  27407  dchrisumlem2  27410  dchrmusum2  27414  dchrvmasumlem2  27418  dchrvmasumlem3  27419  dchrisum0flblem2  27429  dchrisum0fno1  27431  dchrisum0re  27433  dchrisum0lem1  27436  dchrisum0lem2a  27437  mudivsum  27450  mulogsumlem  27451  mulog2sumlem2  27455  vmalogdivsum2  27458  selberglem2  27466  selbergb  27469  selberg2b  27472  logdivbnd  27476  selberg3lem1  27477  selberg3lem2  27478  selberg4lem1  27480  pntrmax  27484  pntrlog2bndlem2  27498  pntrlog2bndlem3  27499  pntrlog2bndlem5  27501  pntrlog2bndlem6a  27502  pntrlog2bndlem6  27503  pntrlog2bnd  27504  pntpbnd1a  27505  pntpbnd1  27506  pntpbnd2  27507  pntibndlem1  27509  pntibndlem2  27511  pntlemb  27517  pntlemq  27521  pntlemr  27522  pntlemj  27523  pntlemk  27526  qabvle  27545  padicabvcxp  27552  ostth2lem2  27554  ostth2lem3  27555  ostth2lem4  27556  ostth3  27558  addsuniflem  27905  negsid  27940  negsunif  27954  mulsuniflem  28036  sltmul2  28058  precsexlem9  28100  absmuls  28125  legtrid  28382  legov3  28389  krippenlem  28481  mideulem2  28525  midex  28528  opphllem5  28542  opphllem6  28543  opphl  28545  lmieu  28575  lmiisolem  28587  ttgcontlem1  28682  colinearalglem4  28707  axpaschlem  28738  axcontlem7  28768  nbfusgrlevtxm2  29178  clwlksndivn  29883  eucrct2eupth  30042  nvge0  30470  smcnlem  30494  nmoub3i  30570  nmoub2i  30571  nmlno0lem  30590  minvecolem2  30672  htthlem  30714  norm3dif2  30948  bcs2  30979  chscllem2  31435  eigposi  31633  nmopub2tALT  31706  nmfnleub2  31723  nmlnop0iALT  31792  riesz1  31862  cnlnadjlem2  31865  nmopcoadji  31898  leopsq  31926  leopmul  31931  leopnmid  31935  nmopleid  31936  opsqrlem6  31942  0leopj  31983  hstle1  32023  strlem3a  32049  mdslmd4i  32130  cvexchlem  32165  cdj1i  32230  unidifsnel  32316  unidifsnne  32317  le2halvesd  32509  xlt2addrd  32512  fsumub  32573  wrdt2ind  32656  xrge0tsmsd  32749  fzto1st1  32801  cycpmco2lem4  32828  cycpmco2lem6  32830  cyc3conja  32856  archiabllem1a  32877  archiabllem2a  32880  archiabllem2c  32881  orngsqr  32959  ornglmulle  32960  orngrmulle  32961  orng0le1  32967  fedgmullem1  33259  fedgmullem2  33260  algextdeglem8  33328  metideq  33430  metider  33431  sqsscirc1  33445  esummono  33609  esumpad2  33611  esumle  33613  esumlef  33617  esumcst  33618  esumrnmpt2  33623  esum2d  33648  aean  33799  dya2ub  33826  dya2icoseg  33833  omssubadd  33856  inelcarsg  33867  carsgsigalem  33871  carsggect  33874  carsgclctunlem2  33875  eulerpartlemb  33924  fibp1  33957  sgnmulsgp  34106  signsplypnf  34118  signsply0  34119  fdvposlt  34167  fdvposle  34169  reprgt  34189  logdivsqrle  34218  hgt750lemb  34224  hgt750leme  34226  tgoldbachgtde  34228  subfacval3  34735  sconnpht2  34784  sconnpi1  34785  resconn  34792  snmlff  34875  sinccvglem  35212  faclimlem2  35274  btwnouttr2  35554  dnibndlem5  35893  dnibndlem7  35895  dnibndlem8  35896  dnibndlem9  35897  dnibndlem10  35898  dnibnd  35902  knoppcnlem4  35907  knoppcnlem9  35912  unbdqndv2lem1  35920  unbdqndv2lem2  35921  knoppndvlem11  35933  knoppndvlem12  35934  knoppndvlem14  35936  knoppndvlem15  35937  knoppndvlem17  35939  knoppndvlem18  35940  knoppndvlem19  35941  knoppndvlem21  35943  ltflcei  37016  poimirlem9  37037  poimirlem26  37054  poimirlem27  37055  poimirlem29  37057  heicant  37063  mblfinlem2  37066  mblfinlem3  37067  mblfinlem4  37068  volsupnfl  37073  itg2addnclem  37079  itg2addnclem3  37081  iblmulc2nc  37093  ftc1cnnclem  37099  ftc1anclem6  37106  ftc1anclem7  37107  ftc1anclem8  37108  ftc2nc  37110  dvasin  37112  geomcau  37167  bfplem2  37231  rrncmslem  37240  rrnequiv  37243  lsatcvatlem  38458  islshpcv  38462  atlatmstc  38728  cvlsupr7  38757  cvrval3  38823  cvrval5  38825  cvrexchlem  38829  atcvrj1  38841  cvrat3  38852  cvrat4  38853  atbtwn  38856  1cvratex  38883  hlatexch4  38891  3atlem1  38893  3atlem2  38894  atcvrlln2  38929  atcvrlln  38930  lplnllnneN  38966  llncvrlpln2  38967  4atlem3b  39008  lplncvrlvol2  39025  dalemswapyz  39066  dalemswapyzps  39100  dalem25  39108  dalem39  39121  dalem58  39140  dalem59  39141  lneq2at  39188  lncvrat  39192  dalawlem2  39282  dalawlem3  39283  dalawlem4  39284  dalawlem6  39286  dalawlem9  39289  dalawlem11  39291  dalawlem12  39292  lhpocnle  39426  lhpmcvr3  39435  lhpmcvr5N  39437  lhpmcvr6N  39438  4atexlemunv  39476  4atexlemc  39479  4atexlemex2  39481  lautm  39504  cdlemc2  39602  cdleme5  39650  cdleme11j  39677  cdleme16b  39689  cdlemednpq  39709  cdleme19e  39717  cdleme20i  39727  cdleme22a  39750  cdleme22cN  39752  cdleme22d  39753  cdleme22e  39754  cdleme22eALTN  39755  cdleme22f  39756  cdleme23c  39761  cdleme30a  39788  cdleme35a  39858  cdleme35b  39860  cdleme42h  39892  cdlemeg46rgv  39938  cdlemg8b  40038  cdlemg12e  40057  cdlemg13a  40061  cdlemg17pq  40082  cdlemg18c  40090  cdlemg19  40094  cdlemg21  40096  cdlemg31d  40110  cdlemg33a  40116  tendoid  40183  cdlemk4  40244  cdlemki  40251  cdlemk10  40253  cdlemksv2  40257  cdlemk12  40260  cdlemk14  40264  cdlemk15  40265  cdlemk1u  40269  cdlemk5u  40271  cdlemk12u  40282  cdlemk45  40357  cdlemk48  40360  dia2dimlem1  40474  dia2dimlem2  40475  dia2dimlem3  40476  cdlemm10N  40528  cdlemn2  40605  dihjustlem  40626  dihglbcpreN  40710  dihmeetlem3N  40715  nnproddivdvdsd  41408  lcmineqlem17  41453  lcmineqlem18  41454  3lexlogpow2ineq1  41466  3lexlogpow2ineq2  41467  3lexlogpow5ineq5  41468  aks4d1p1p3  41477  aks4d1p1p2  41478  aks4d1p1p4  41479  aks4d1p1p5  41483  aks4d1p1  41484  aks4d1p3  41486  aks4d1p8  41495  posbezout  41507  aks6d1c1  41520  hashscontpow1  41525  aks6d1c2  41533  aks6d1c5lem1  41539  aks6d1c5lem3  41540  aks6d1c5lem2  41541  deg1gprod  41544  sticksstones7  41556  sticksstones10  41559  sticksstones12  41562  sticksstones22  41572  aks6d1c6lem1  41574  aks6d1c6lem3  41576  2xp3dxp2ge1d  41613  factwoffsmonot  41614  evlselv  41742  zrtdvds  41827  rtprmirr  41828  dffltz  41980  fltdvdsabdvdsc  41984  fltaccoprm  41986  fltabcoprm  41988  flt4lem5elem  41997  flt4lem7  42005  fltnlta  42009  irrapxlem1  42164  pell1qrgaplem  42215  pell1qrgap  42216  monotoddzzfi  42285  jm2.24nn  42302  congtr  42308  congmul  42310  congsub  42313  fzmaxdif  42324  acongeq  42326  jm2.20nn  42340  jm2.25  42342  hbtlem4  42472  dgrsub2  42481  mpaaeu  42496  idomsubgmo  42543  iscard4  42886  sqrtcvallem4  42992  leeq2d  43511  int-sqgeq0d  43539  int-ineqmvtd  43544  cvgdvgrat  43673  radcnvrat  43674  hashnzfzclim  43682  dvconstbi  43694  binomcxplemdvbinom  43713  isosctrlem1ALT  44296  mulltgt0  44307  rnmptbd2lem  44547  oddfl  44582  2timesgt  44593  lt3addmuld  44606  lt4addmuld  44611  supxrgere  44638  supxrgelem  44642  supxrge  44643  xadd0ge2  44646  infrpge  44656  xrlexaddrp  44657  xralrple2  44659  infxr  44672  infleinflem1  44675  infleinflem2  44676  infleinf  44677  xralrple4  44678  xralrple3  44679  recnnltrp  44682  rpgtrecnn  44685  xrralrecnnge  44695  rexabslelem  44723  infrnmptle  44728  supminfxr  44769  xrpnf  44791  iccshift  44826  iooshift  44830  ressiocsup  44862  ressioosup  44863  fsumnncl  44883  fmul01  44891  fmul01lt1lem1  44895  fmul01lt1lem2  44896  mccllem  44908  climrec  44914  climexp  44916  climneg  44921  limcrecl  44940  sumnnodd  44941  lptioo2  44942  lptioo1  44943  ltmod  44949  lptre2pt  44951  0ellimcdiv  44960  limclner  44962  fnlimcnv  44978  climinf2lem  45017  limsupubuzlem  45023  limsup10exlem  45083  limsupgtlem  45088  dfxlim2v  45158  xlimliminflimsup  45173  cncficcgt0  45199  cncfioobdlem  45207  ioodvbdlimc1lem1  45242  ioodvbdlimc1lem2  45243  ioodvbdlimc2lem  45245  dvdsn1add  45250  dvnxpaek  45253  dvnmul  45254  dvnprodlem1  45257  itgiccshift  45291  itgperiod  45292  sublevolico  45295  ismbl3  45297  ovolsplit  45299  ismbl4  45304  stoweidlem1  45312  stoweidlem11  45322  stoweidlem13  45324  stoweidlem26  45337  stoweidlem34  45345  stoweidlem38  45349  stoweidlem42  45353  stoweidlem51  45362  stoweidlem59  45370  stirlinglem5  45389  stirlinglem6  45390  stirlinglem7  45391  stirlinglem10  45394  stirlinglem11  45395  stirlinglem13  45397  stirlinglem15  45399  dirkercncflem1  45414  dirkercncflem4  45417  fourierdlem4  45422  fourierdlem10  45428  fourierdlem11  45429  fourierdlem15  45433  fourierdlem20  45438  fourierdlem25  45443  fourierdlem26  45444  fourierdlem30  45448  fourierdlem37  45455  fourierdlem39  45457  fourierdlem40  45458  fourierdlem41  45459  fourierdlem42  45460  fourierdlem44  45462  fourierdlem47  45464  fourierdlem48  45465  fourierdlem49  45466  fourierdlem50  45467  fourierdlem51  45468  fourierdlem52  45469  fourierdlem54  45471  fourierdlem60  45477  fourierdlem61  45478  fourierdlem63  45480  fourierdlem64  45481  fourierdlem65  45482  fourierdlem73  45490  fourierdlem74  45491  fourierdlem75  45492  fourierdlem76  45493  fourierdlem78  45495  fourierdlem79  45496  fourierdlem81  45498  fourierdlem84  45501  fourierdlem87  45504  fourierdlem92  45509  fourierdlem93  45510  fourierdlem101  45518  fourierdlem102  45519  fourierdlem103  45520  fourierdlem104  45521  fourierdlem111  45528  fourierdlem114  45531  sqwvfoura  45539  sqwvfourb  45540  fouriersw  45542  etransclem19  45564  etransclem23  45568  etransclem24  45569  etransclem25  45570  etransclem27  45572  etransclem32  45577  etransclem35  45580  etransclem48  45593  qndenserrnbllem  45605  ioorrnopnlem  45615  ioorrnopnxrlem  45617  fsumlesge0  45688  sge0cl  45692  sge0supre  45700  sge0less  45703  sge0gerp  45706  sge0ltfirp  45711  sge0le  45718  sge0ltfirpmpt  45719  sge0split  45720  sge0rpcpnf  45732  sge0ltfirpmpt2  45737  sge0isum  45738  sge0xaddlem1  45744  sge0pnffigtmpt  45751  sge0pnffsumgt  45753  sge0gtfsumgt  45754  sge0seq  45757  nnfoctbdjlem  45766  meassle  45774  meaiuninclem  45791  meaiininclem  45797  omeiunle  45828  omeiunltfirp  45830  carageniuncllem2  45833  carageniuncl  45834  omess0  45845  hoicvr  45859  ovnlerp  45873  ovnsubaddlem1  45881  hsphoidmvle2  45896  hoidmv1lelem2  45903  hoidmv1le  45905  hoidmvlelem1  45906  hoidmvlelem2  45907  hoidmvlelem3  45908  hoidmvlelem5  45910  ovnhoilem2  45913  ovnhoi  45914  hoidifhspdmvle  45931  hoiqssbllem2  45934  hspmbllem2  45938  hspmbllem3  45939  hspmbl  45940  vonioolem2  45992  vonicclem2  45995  smfaddlem1  46074  smflimlem2  46083  smflimlem4  46085  smfmullem1  46102  smfinflem  46128  smflimsuplem4  46134  smflimsuplem8  46138  perfectALTVlem2  46985  nnpw2blen  47576  itscnhlinecirc02plem1  47778