MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  breqtrd Structured version   Visualization version   GIF version

Theorem breqtrd 5132
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
StepHypRef Expression
1 breqtrd.1 . 2 (𝜑𝐴𝑅𝐵)
2 breqtrd.2 . . 3 (𝜑𝐵 = 𝐶)
32breq2d 5118 . 2 (𝜑 → (𝐴𝑅𝐵𝐴𝑅𝐶))
41, 3mpbid 231 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542   class class class wbr 5106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107
This theorem is referenced by:  breqtrrd  5134  breqtrid  5143  domunsn  9072  mapdom2  9093  phplem2  9153  phplem4OLD  9165  mapfien2  9346  wemaplem2  9484  infdifsn  9594  cantnff  9611  ttrclss  9657  rnttrcl  9659  infxpenlem  9950  infmap2  10155  ssfin4  10247  canthp1lem1  10589  nqereq  10872  ltexnq  10912  ltbtwnnq  10915  add20  11668  mullt0  11675  ltm1  11998  recgt0  12002  prodgt0  12003  ltmul1a  12005  mulge0b  12026  recp1lt1  12054  recreclt  12055  ledivp1  12058  ledivp1i  12081  ltdivp1i  12082  eluzmn  12771  ltaddrp2d  12992  mul2lt0bi  13022  prodge0rd  13023  xleadd1a  13173  xov1plusxeqvd  13416  fz01en  13470  fzonmapblen  13619  fladdz  13731  flhalf  13736  fldiv  13766  modsubdir  13846  fzen2  13875  serle  13964  ltexp2a  14072  leexp2a  14078  exple1  14082  expubnd  14083  bernneq  14133  expmulnbnd  14139  discr1  14143  discr  14144  faclbnd6  14200  hashfz  14328  hashfun  14338  seqcoll  14364  sqeqd  15052  01sqrexlem7  15134  sqrtge0  15143  sqrtneglem  15152  abslt  15200  absle  15201  abstri  15216  rlimge0  15464  reccn2  15480  climaddc2  15519  isercolllem1  15550  caucvgrlem  15558  summolem2a  15601  isumge0  15652  fsumle  15685  fsumlt  15686  o1fsum  15699  supcvg  15742  expcnv  15750  geolim  15756  geolim2  15757  georeclim  15758  geo2lim  15761  mertenslem1  15770  mertens  15772  prodmolem2a  15818  efcllem  15961  ef0lem  15962  efgt0  15986  eftlub  15992  eflt  16000  sinbnd  16063  cosbnd  16064  ef01bndlem  16067  sin01gt0  16073  cos01gt0  16074  sin02gt0  16075  eirrlem  16087  rpnnen2lem11  16107  rpnnen2lem12  16108  ruclem11  16123  dvdssub2  16184  dvdsadd2b  16189  dvdsexp  16211  3dvds  16214  opoe  16246  bitsfzolem  16315  bitsinv1lem  16322  bezoutlem4  16424  dvdsgcd  16426  dvdsmulgcd  16437  bezoutr1  16446  nn0seqcvgd  16447  rpmulgcd2  16533  qredeq  16534  rpdvds  16537  prmind2  16562  divdenle  16625  hashdvds  16648  phimullem  16652  eulerthlem2  16655  prmdiveq  16659  prmdivdiv  16660  pythagtriplem4  16692  pythagtriplem10  16693  pythagtriplem19  16706  iserodd  16708  pcpre1  16715  pcadd2  16763  qexpz  16774  expnprm  16775  oddprmdvds  16776  pockthlem  16778  prmreclem2  16790  prmreclem3  16791  4sqlem7  16817  4sqlem10  16820  4sqlem11  16828  4sqlem12  16829  4sqlem14  16831  4sqlem15  16832  4sqlem16  16833  0ram  16893  ffthiso  17817  latmlej12  18369  qusgrp  18986  pgpfi1  19378  sylow1lem4  19384  sylow1lem5  19385  odcau  19387  pgpfi  19388  pgpssslw  19397  sylow3lem4  19413  sylow3lem6  19415  efgsfo  19522  frgp0  19543  odadd1  19627  odadd2  19628  odadd  19629  gexexlem  19631  lt6abl  19673  gsumzsubmcl  19696  pwsgsum  19760  dprd2dlem1  19821  dprd2d2  19824  ablfacrplem  19845  ablfacrp  19846  ablfacrp2  19847  ablfac1b  19850  ablfac1eu  19853  pgpfac1lem3a  19856  ablfaclem2  19866  dvdsrid  20081  dvdsrtr  20082  dvdsrneg  20084  unitmulcl  20094  unitgrp  20097  unitnegcl  20111  isdrng2  20199  subrguss  20240  subrgunit  20243  abvsubtri  20297  fidomndrnglem  20780  gzrngunit  20866  prmirredlem  20896  znidomb  20971  frlmgsum  21181  psrbaglesupp  21329  psrbaglesuppOLD  21330  invrvald  22028  psmetsym  23666  psmettri  23667  mettri2  23697  xmetsym  23703  xmettri  23707  prdsxmetlem  23724  xblss2ps  23757  xblss2  23758  blhalf  23761  xmsge0  23819  ngptgp  23995  nrginvrcnlem  24058  nmoeq0  24103  cnmet  24138  blcvx  24164  opnreen  24197  metdcnlem  24202  metdstri  24217  metdsle  24218  metnrmlem1  24225  metnrmlem3  24227  lebnumlem1  24327  pi1inv  24418  cphnmf  24562  ipge0  24565  ipcau2  24601  tcphcphlem1  24602  csbren  24766  minveclem2  24793  minveclem3  24796  ovolssnul  24854  ovolctb  24857  ovolunnul  24867  ovoliunlem1  24869  ovoliun2  24873  ovoliunnul  24874  ioombl1lem4  24928  uniioombllem3  24952  uniioombllem4  24953  uniioombllem5  24954  uniioombl  24956  volcn  24973  vitalilem2  24976  vitalilem5  24979  itg1lea  25080  mbfi1fseqlem6  25088  mbfi1flimlem  25090  itg2eqa  25113  itg2splitlem  25116  itg2split  25117  itg2monolem1  25118  itg2cnlem2  25130  iblabsr  25197  iblmulc2  25198  bddiblnc  25209  dveflem  25346  dvef  25347  dvferm2lem  25353  dvlip  25360  c1liplem1  25363  dveq0  25367  dvlt0  25372  dvivthlem1  25375  lhop1  25381  dvfsumle  25388  dvfsumlem4  25396  dvfsumrlim3  25400  dvfsum2  25401  ftc1a  25404  ftc1lem4  25406  deg1add  25471  ply1divex  25504  ply1rem  25531  fta1glem2  25534  fta1blem  25536  ig1pdvds  25544  plyeq0lem  25574  dgrcolem2  25638  plydivlem4  25659  plyrem  25668  fta1lem  25670  aalioulem3  25697  aaliou2b  25704  aaliou3lem3  25707  aaliou3lem8  25708  ulmcn  25761  ulmdvlem1  25762  itgulm  25770  pserulm  25784  pserdvlem2  25790  abelthlem2  25794  abelthlem5  25797  abelthlem6  25798  abelthlem7  25800  abelthlem8  25801  abelthlem9  25802  sinq12gt0  25867  sinq34lt0t  25869  cosq14gt0  25870  cosq14ge0  25871  cos02pilt1  25885  efif1olem3  25903  argimgt0  25970  argimlt0  25971  logneg2  25973  logcnlem3  26002  logcnlem4  26003  logtayllem  26017  logtayl2  26020  cxpsqrtlem  26060  cxpsqrt  26061  cxpaddlelem  26107  abscxpbnd  26109  loglesqrt  26114  ang180lem2  26163  atanlogaddlem  26266  atanlogsublem  26268  atantan  26276  atans2  26284  atantayl  26290  leibpi  26295  log2tlbnd  26298  birthdaylem2  26305  birthdaylem3  26306  cxp2limlem  26328  jensenlem2  26340  jensen  26341  logdiflbnd  26347  emcllem2  26349  emcllem4  26351  harmonicbnd4  26363  fsumharmonic  26364  lgamgulmlem2  26382  lgamgulm2  26388  lgambdd  26389  lgamucov  26390  lgamcvglem  26392  lgamcvg2  26407  gamcvg  26408  wilthlem3  26422  basellem1  26433  basellem3  26435  basellem4  26436  fsumdvdsdiaglem  26535  dvdsppwf1o  26538  dvdsmulf1o  26546  chteq0  26560  chtub  26563  chpub  26571  logfacubnd  26572  logfaclbnd  26573  logexprlim  26576  perfectlem2  26581  dchrfi  26606  bclbnd  26631  bposlem1  26635  bposlem3  26637  bposlem4  26638  bposlem6  26640  lgslem1  26648  lgsqrlem2  26698  lgsqrlem4  26700  lgseisenlem2  26727  lgsquadlem1  26731  lgsquadlem2  26732  lgsquad2lem1  26735  2sqlem3  26771  2sqlem4  26772  2sqlem8  26777  2sqlem11  26780  2sqcoprm  26786  2sqmod  26787  chebbnd1lem2  26821  chebbnd1lem3  26822  chtppilimlem1  26824  chpchtlim  26830  vmadivsum  26833  vmadivsumb  26834  rpvmasumlem  26838  dchrisumlem2  26841  dchrmusum2  26845  dchrvmasumlem2  26849  dchrvmasumlem3  26850  dchrisum0flblem2  26860  dchrisum0fno1  26862  dchrisum0re  26864  dchrisum0lem1  26867  dchrisum0lem2a  26868  mudivsum  26881  mulogsumlem  26882  mulog2sumlem2  26886  vmalogdivsum2  26889  selberglem2  26897  selbergb  26900  selberg2b  26903  logdivbnd  26907  selberg3lem1  26908  selberg3lem2  26909  selberg4lem1  26911  pntrmax  26915  pntrlog2bndlem2  26929  pntrlog2bndlem3  26930  pntrlog2bndlem5  26932  pntrlog2bndlem6a  26933  pntrlog2bndlem6  26934  pntrlog2bnd  26935  pntpbnd1a  26936  pntpbnd1  26937  pntpbnd2  26938  pntibndlem1  26940  pntibndlem2  26942  pntlemb  26948  pntlemq  26952  pntlemr  26953  pntlemj  26954  pntlemk  26957  qabvle  26976  padicabvcxp  26983  ostth2lem2  26985  ostth2lem3  26986  ostth2lem4  26987  ostth3  26989  addsunif  27313  negsid  27342  negsunif  27353  legtrid  27536  legov3  27543  krippenlem  27635  mideulem2  27679  midex  27682  opphllem5  27696  opphllem6  27697  opphl  27699  lmieu  27729  lmiisolem  27741  ttgcontlem1  27836  colinearalglem4  27861  axpaschlem  27892  axcontlem7  27922  nbfusgrlevtxm2  28329  clwlksndivn  29033  eucrct2eupth  29192  nvge0  29618  smcnlem  29642  nmoub3i  29718  nmoub2i  29719  nmlno0lem  29738  minvecolem2  29820  htthlem  29862  norm3dif2  30096  bcs2  30127  chscllem2  30583  eigposi  30781  nmopub2tALT  30854  nmfnleub2  30871  nmlnop0iALT  30940  riesz1  31010  cnlnadjlem2  31013  nmopcoadji  31046  leopsq  31074  leopmul  31079  leopnmid  31083  nmopleid  31084  opsqrlem6  31090  0leopj  31131  hstle1  31171  strlem3a  31197  mdslmd4i  31278  cvexchlem  31313  cdj1i  31378  unidifsnel  31465  unidifsnne  31466  le2halvesd  31663  xlt2addrd  31666  fsumub  31727  wrdt2ind  31810  xrge0tsmsd  31902  fzto1st1  31954  cycpmco2lem4  31981  cycpmco2lem6  31983  cyc3conja  32009  archiabllem1a  32030  archiabllem2a  32033  archiabllem2c  32034  orngsqr  32102  ornglmulle  32103  orngrmulle  32104  orng0le1  32110  fedgmullem1  32327  fedgmullem2  32328  metideq  32477  metider  32478  sqsscirc1  32492  esummono  32656  esumpad2  32658  esumle  32660  esumlef  32664  esumcst  32665  esumrnmpt2  32670  esum2d  32695  aean  32846  dya2ub  32873  dya2icoseg  32880  omssubadd  32903  inelcarsg  32914  carsgsigalem  32918  carsggect  32921  carsgclctunlem2  32922  eulerpartlemb  32971  fibp1  33004  sgnmulsgp  33153  signsplypnf  33165  signsply0  33166  fdvposlt  33215  fdvposle  33217  reprgt  33237  logdivsqrle  33266  hgt750lemb  33272  hgt750leme  33274  tgoldbachgtde  33276  subfacval3  33786  sconnpht2  33835  sconnpi1  33836  resconn  33843  snmlff  33926  sinccvglem  34263  faclimlem2  34320  btwnouttr2  34610  dnibndlem5  34948  dnibndlem7  34950  dnibndlem8  34951  dnibndlem9  34952  dnibndlem10  34953  dnibnd  34957  knoppcnlem4  34962  knoppcnlem9  34967  unbdqndv2lem1  34975  unbdqndv2lem2  34976  knoppndvlem11  34988  knoppndvlem12  34989  knoppndvlem14  34991  knoppndvlem15  34992  knoppndvlem17  34994  knoppndvlem18  34995  knoppndvlem19  34996  knoppndvlem21  34998  ltflcei  36069  poimirlem9  36090  poimirlem26  36107  poimirlem27  36108  poimirlem29  36110  heicant  36116  mblfinlem2  36119  mblfinlem3  36120  mblfinlem4  36121  volsupnfl  36126  itg2addnclem  36132  itg2addnclem3  36134  iblmulc2nc  36146  ftc1cnnclem  36152  ftc1anclem6  36159  ftc1anclem7  36160  ftc1anclem8  36161  ftc2nc  36163  dvasin  36165  geomcau  36221  bfplem2  36285  rrncmslem  36294  rrnequiv  36297  lsatcvatlem  37514  islshpcv  37518  atlatmstc  37784  cvlsupr7  37813  cvrval3  37879  cvrval5  37881  cvrexchlem  37885  atcvrj1  37897  cvrat3  37908  cvrat4  37909  atbtwn  37912  1cvratex  37939  hlatexch4  37947  3atlem1  37949  3atlem2  37950  atcvrlln2  37985  atcvrlln  37986  lplnllnneN  38022  llncvrlpln2  38023  4atlem3b  38064  lplncvrlvol2  38081  dalemswapyz  38122  dalemswapyzps  38156  dalem25  38164  dalem39  38177  dalem58  38196  dalem59  38197  lneq2at  38244  lncvrat  38248  dalawlem2  38338  dalawlem3  38339  dalawlem4  38340  dalawlem6  38342  dalawlem9  38345  dalawlem11  38347  dalawlem12  38348  lhpocnle  38482  lhpmcvr3  38491  lhpmcvr5N  38493  lhpmcvr6N  38494  4atexlemunv  38532  4atexlemc  38535  4atexlemex2  38537  lautm  38560  cdlemc2  38658  cdleme5  38706  cdleme11j  38733  cdleme16b  38745  cdlemednpq  38765  cdleme19e  38773  cdleme20i  38783  cdleme22a  38806  cdleme22cN  38808  cdleme22d  38809  cdleme22e  38810  cdleme22eALTN  38811  cdleme22f  38812  cdleme23c  38817  cdleme30a  38844  cdleme35a  38914  cdleme35b  38916  cdleme42h  38948  cdlemeg46rgv  38994  cdlemg8b  39094  cdlemg12e  39113  cdlemg13a  39117  cdlemg17pq  39138  cdlemg18c  39146  cdlemg19  39150  cdlemg21  39152  cdlemg31d  39166  cdlemg33a  39172  tendoid  39239  cdlemk4  39300  cdlemki  39307  cdlemk10  39309  cdlemksv2  39313  cdlemk12  39316  cdlemk14  39320  cdlemk15  39321  cdlemk1u  39325  cdlemk5u  39327  cdlemk12u  39338  cdlemk45  39413  cdlemk48  39416  dia2dimlem1  39530  dia2dimlem2  39531  dia2dimlem3  39532  cdlemm10N  39584  cdlemn2  39661  dihjustlem  39682  dihglbcpreN  39766  dihmeetlem3N  39771  nnproddivdvdsd  40461  lcmineqlem17  40505  lcmineqlem18  40506  3lexlogpow2ineq1  40518  3lexlogpow2ineq2  40519  3lexlogpow5ineq5  40520  aks4d1p1p3  40529  aks4d1p1p2  40530  aks4d1p1p4  40531  aks4d1p1p5  40535  aks4d1p1  40536  aks4d1p3  40538  aks4d1p8  40547  sticksstones7  40563  sticksstones10  40566  sticksstones12  40569  sticksstones22  40579  2xp3dxp2ge1d  40617  factwoffsmonot  40618  zrtdvds  40835  rtprmirr  40836  dffltz  40975  fltdvdsabdvdsc  40979  fltaccoprm  40981  fltabcoprm  40983  flt4lem5elem  40992  flt4lem7  41000  fltnlta  41004  irrapxlem1  41148  pell1qrgaplem  41199  pell1qrgap  41200  monotoddzzfi  41269  jm2.24nn  41286  congtr  41292  congmul  41294  congsub  41297  fzmaxdif  41308  acongeq  41310  jm2.20nn  41324  jm2.25  41326  hbtlem4  41456  dgrsub2  41465  mpaaeu  41480  idomsubgmo  41528  iscard4  41812  sqrtcvallem4  41918  leeq2d  42437  int-sqgeq0d  42466  int-ineqmvtd  42471  cvgdvgrat  42600  radcnvrat  42601  hashnzfzclim  42609  dvconstbi  42621  binomcxplemdvbinom  42640  isosctrlem1ALT  43223  mulltgt0  43234  rnmptbd2lem  43483  oddfl  43518  2timesgt  43529  lt3addmuld  43542  lt4addmuld  43547  supxrgere  43574  supxrgelem  43578  supxrge  43579  xadd0ge2  43582  infrpge  43592  xrlexaddrp  43593  xralrple2  43595  infxr  43608  infleinflem1  43611  infleinflem2  43612  infleinf  43613  xralrple4  43614  xralrple3  43615  recnnltrp  43618  rpgtrecnn  43621  xrralrecnnge  43632  rexabslelem  43660  infrnmptle  43665  supminfxr  43706  xrpnf  43728  iccshift  43763  iooshift  43767  ressiocsup  43799  ressioosup  43800  fsumnncl  43820  fmul01  43828  fmul01lt1lem1  43832  fmul01lt1lem2  43833  mccllem  43845  climrec  43851  climexp  43853  climneg  43858  limcrecl  43877  sumnnodd  43878  lptioo2  43879  lptioo1  43880  ltmod  43886  lptre2pt  43888  0ellimcdiv  43897  limclner  43899  fnlimcnv  43915  climinf2lem  43954  limsupubuzlem  43960  limsup10exlem  44020  limsupgtlem  44025  dfxlim2v  44095  xlimliminflimsup  44110  cncficcgt0  44136  cncfioobdlem  44144  ioodvbdlimc1lem1  44179  ioodvbdlimc1lem2  44180  ioodvbdlimc2lem  44182  dvdsn1add  44187  dvnxpaek  44190  dvnmul  44191  dvnprodlem1  44194  itgiccshift  44228  itgperiod  44229  sublevolico  44232  ismbl3  44234  ovolsplit  44236  ismbl4  44241  stoweidlem1  44249  stoweidlem11  44259  stoweidlem13  44261  stoweidlem26  44274  stoweidlem34  44282  stoweidlem38  44286  stoweidlem42  44290  stoweidlem51  44299  stoweidlem59  44307  stirlinglem5  44326  stirlinglem6  44327  stirlinglem7  44328  stirlinglem10  44331  stirlinglem11  44332  stirlinglem13  44334  stirlinglem15  44336  dirkercncflem1  44351  dirkercncflem4  44354  fourierdlem4  44359  fourierdlem10  44365  fourierdlem11  44366  fourierdlem15  44370  fourierdlem20  44375  fourierdlem25  44380  fourierdlem26  44381  fourierdlem30  44385  fourierdlem37  44392  fourierdlem39  44394  fourierdlem40  44395  fourierdlem41  44396  fourierdlem42  44397  fourierdlem44  44399  fourierdlem47  44401  fourierdlem48  44402  fourierdlem49  44403  fourierdlem50  44404  fourierdlem51  44405  fourierdlem52  44406  fourierdlem54  44408  fourierdlem60  44414  fourierdlem61  44415  fourierdlem63  44417  fourierdlem64  44418  fourierdlem65  44419  fourierdlem73  44427  fourierdlem74  44428  fourierdlem75  44429  fourierdlem76  44430  fourierdlem78  44432  fourierdlem79  44433  fourierdlem81  44435  fourierdlem84  44438  fourierdlem87  44441  fourierdlem92  44446  fourierdlem93  44447  fourierdlem101  44455  fourierdlem102  44456  fourierdlem103  44457  fourierdlem104  44458  fourierdlem111  44465  fourierdlem114  44468  sqwvfoura  44476  sqwvfourb  44477  fouriersw  44479  etransclem19  44501  etransclem23  44505  etransclem24  44506  etransclem25  44507  etransclem27  44509  etransclem32  44514  etransclem35  44517  etransclem48  44530  qndenserrnbllem  44542  ioorrnopnlem  44552  ioorrnopnxrlem  44554  fsumlesge0  44625  sge0cl  44629  sge0supre  44637  sge0less  44640  sge0gerp  44643  sge0ltfirp  44648  sge0le  44655  sge0ltfirpmpt  44656  sge0split  44657  sge0rpcpnf  44669  sge0ltfirpmpt2  44674  sge0isum  44675  sge0xaddlem1  44681  sge0pnffigtmpt  44688  sge0pnffsumgt  44690  sge0gtfsumgt  44691  sge0seq  44694  nnfoctbdjlem  44703  meassle  44711  meaiuninclem  44728  meaiininclem  44734  omeiunle  44765  omeiunltfirp  44767  carageniuncllem2  44770  carageniuncl  44771  omess0  44782  hoicvr  44796  ovnlerp  44810  ovnsubaddlem1  44818  hsphoidmvle2  44833  hoidmv1lelem2  44840  hoidmv1le  44842  hoidmvlelem1  44843  hoidmvlelem2  44844  hoidmvlelem3  44845  hoidmvlelem5  44847  ovnhoilem2  44850  ovnhoi  44851  hoidifhspdmvle  44868  hoiqssbllem2  44871  hspmbllem2  44875  hspmbllem3  44876  hspmbl  44877  vonioolem2  44929  vonicclem2  44932  smfaddlem1  45011  smflimlem2  45020  smflimlem4  45022  smfmullem1  45039  smfinflem  45065  smflimsuplem4  45071  smflimsuplem8  45075  perfectALTVlem2  45921  nnpw2blen  46673  itscnhlinecirc02plem1  46875
  Copyright terms: Public domain W3C validator