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

Theorem breqtrd 4603
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 4589 . 2 (𝜑 → (𝐴𝑅𝐵𝐴𝑅𝐶))
41, 3mpbid 220 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474   class class class wbr 4577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578
This theorem is referenced by:  breqtrrd  4605  syl5breq  4614  domunsn  7972  mapdom2  7993  phplem4  8004  mapfien2  8174  wemaplem2  8312  infdifsn  8414  cantnff  8431  infxpenlem  8696  pwcda1  8876  pwcdadom  8898  infmap2  8900  ssfin4  8992  canthp1lem1  9330  nqereq  9613  ltexnq  9653  ltbtwnnq  9656  add20  10389  mullt0  10396  ltm1  10712  recgt0  10716  prodgt0  10717  prodge0  10719  ltmul1a  10721  mulge0b  10742  recp1lt1  10770  recreclt  10771  ledivp1  10774  ledivp1i  10798  ltdivp1i  10799  eluzmn  11526  ltaddrp2d  11738  mul2lt0bi  11768  xleadd1a  11912  xov1plusxeqvd  12145  fz01en  12195  fzonmapblen  12336  fladdz  12443  flhalf  12448  fldiv  12476  modsubdir  12556  fzen2  12585  serle  12673  ltexp2a  12729  leexp2a  12733  exple1  12737  expubnd  12738  bernneq  12807  expmulnbnd  12813  discr1  12817  discr  12818  faclbnd6  12903  hashfz  13026  hashfun  13036  seqcoll  13057  sqeqd  13700  sqrlem7  13783  sqrtge0  13792  sqrtneglem  13801  abslt  13848  absle  13849  abstri  13864  rlimge0  14106  reccn2  14121  climaddc2  14160  isercolllem1  14189  caucvgrlem  14197  summolem2a  14239  isumge0  14285  fsumle  14318  fsumlt  14319  o1fsum  14332  supcvg  14373  expcnv  14381  geolim  14386  geolim2  14387  georeclim  14388  geo2lim  14391  mertenslem1  14401  mertens  14403  prodmolem2a  14449  efcllem  14593  ef0lem  14594  efgt0  14618  eftlub  14624  eflt  14632  sinbnd  14695  cosbnd  14696  ef01bndlem  14699  sin01gt0  14705  cos01gt0  14706  sin02gt0  14707  eirrlem  14717  rpnnen2lem11  14738  rpnnen2lem12  14739  ruclem11  14754  dvdssub2  14807  dvdsadd2b  14812  dvdsexp  14833  3dvds  14836  3dvdsOLD  14837  opoe  14871  bitsfzolem  14940  bitsinv1lem  14947  bezoutlem4  15043  dvdsgcd  15045  dvdsmulgcd  15058  bezoutr1  15066  nn0seqcvgd  15067  rpmulgcd2  15154  qredeq  15155  rpdvds  15158  prmind2  15182  divdenle  15241  hashdvds  15264  phimullem  15268  eulerthlem2  15271  prmdiveq  15275  prmdivdiv  15276  pythagtriplem4  15308  pythagtriplem10  15309  pythagtriplem19  15322  iserodd  15324  pcpre1  15331  pcadd2  15378  qexpz  15389  expnprm  15390  oddprmdvds  15391  pockthlem  15393  prmreclem2  15405  prmreclem3  15406  4sqlem7  15432  4sqlem10  15435  4sqlem11  15443  4sqlem12  15444  4sqlem14  15446  4sqlem15  15447  4sqlem16  15448  0ram  15508  ffthiso  16358  latmlej12  16860  qusgrp  17418  pgpfi1  17779  sylow1lem4  17785  sylow1lem5  17786  odcau  17788  pgpfi  17789  pgpssslw  17798  sylow3lem4  17814  sylow3lem6  17816  efgsfo  17921  frgp0  17942  odadd1  18020  odadd2  18021  odadd  18022  gexexlem  18024  lt6abl  18065  gsumzsubmcl  18087  pwsgsum  18147  dprd2dlem1  18209  dprd2d2  18212  ablfacrplem  18233  ablfacrp  18234  ablfacrp2  18235  ablfac1b  18238  ablfac1eu  18241  pgpfac1lem3a  18244  ablfaclem2  18254  dvdsrid  18420  dvdsrtr  18421  dvdsrneg  18423  unitmulcl  18433  unitgrp  18436  unitnegcl  18450  isdrng2  18526  subrguss  18564  subrgunit  18567  abvsubtri  18604  fidomndrnglem  19073  psrbaglesupp  19135  gzrngunit  19577  prmirredlem  19605  znidomb  19674  frlmgsum  19872  invrvald  20243  psmetsym  21867  psmettri  21868  mettri2  21897  xmetsym  21903  xmettri  21907  prdsxmetlem  21924  xblss2ps  21957  xblss2  21958  blhalf  21961  xmsge0  22019  ngptgp  22188  nrginvrcnlem  22238  nmoeq0  22282  cnmet  22317  blcvx  22341  opnreen  22374  metdcnlem  22379  metdstri  22393  metdsle  22394  metnrmlem1  22401  metnrmlem3  22403  lebnumlem1  22499  pi1inv  22591  cphnmf  22727  ipge0  22730  ipcau2  22762  tchcphlem1  22763  csbren  22907  minveclem2  22922  minveclem3  22925  ovolssnul  22979  ovolctb  22982  ovolunnul  22992  ovoliunlem1  22994  ovoliun2  22998  ovoliunnul  22999  ioombl1lem4  23053  uniioombllem3  23076  uniioombllem4  23077  uniioombllem5  23078  uniioombl  23080  volcn  23097  vitalilem2  23101  vitalilem5  23104  itg1lea  23202  mbfi1fseqlem6  23210  mbfi1flimlem  23212  itg2eqa  23235  itg2splitlem  23238  itg2split  23239  itg2monolem1  23240  itg2cnlem2  23252  iblabsr  23319  iblmulc2  23320  dveflem  23463  dvef  23464  dvferm2lem  23470  dvlip  23477  c1liplem1  23480  dveq0  23484  dvlt0  23489  dvivthlem1  23492  lhop1  23498  dvfsumle  23505  dvfsumlem4  23513  dvfsumrlim3  23517  dvfsum2  23518  ftc1a  23521  ftc1lem4  23523  deg1add  23584  ply1divex  23617  ply1rem  23644  fta1glem2  23647  fta1blem  23649  ig1pdvds  23657  plyeq0lem  23687  dgrcolem2  23751  plydivlem4  23772  plyrem  23781  fta1lem  23783  aalioulem3  23810  aaliou2b  23817  aaliou3lem3  23820  aaliou3lem8  23821  ulmcn  23874  ulmdvlem1  23875  itgulm  23883  pserulm  23897  pserdvlem2  23903  abelthlem2  23907  abelthlem5  23910  abelthlem6  23911  abelthlem7  23913  abelthlem8  23914  abelthlem9  23915  sinq12gt0  23980  sinq34lt0t  23982  cosq14gt0  23983  cosq14ge0  23984  efif1olem3  24011  argimgt0  24079  argimlt0  24080  logneg2  24082  logcnlem3  24107  logcnlem4  24108  logtayllem  24122  logtayl2  24125  cxpsqrtlem  24165  cxpsqrt  24166  cxpaddlelem  24209  abscxpbnd  24211  loglesqrt  24216  ang180lem2  24257  atanlogaddlem  24357  atanlogsublem  24359  atantan  24367  atans2  24375  atantayl  24381  leibpi  24386  log2tlbnd  24389  birthdaylem2  24396  birthdaylem3  24397  cxp2limlem  24419  jensenlem2  24431  jensen  24432  logdiflbnd  24438  emcllem2  24440  emcllem4  24442  harmonicbnd4  24454  fsumharmonic  24455  lgamgulmlem2  24473  lgamgulm2  24479  lgambdd  24480  lgamucov  24481  lgamcvglem  24483  lgamcvg2  24498  gamcvg  24499  wilthlem3  24513  basellem1  24524  basellem3  24526  basellem4  24527  fsumdvdsdiaglem  24626  dvdsppwf1o  24629  dvdsmulf1o  24637  chteq0  24651  chtub  24654  chpub  24662  logfacubnd  24663  logfaclbnd  24664  logexprlim  24667  perfectlem2  24672  dchrfi  24697  bclbnd  24722  bposlem1  24726  bposlem3  24728  bposlem4  24729  bposlem6  24731  lgslem1  24739  lgsqrlem2  24789  lgsqrlem4  24791  lgseisenlem2  24818  lgsquadlem1  24822  lgsquadlem2  24823  lgsquad2lem1  24826  2sqlem3  24862  2sqlem4  24863  2sqlem8  24868  2sqlem11  24871  chebbnd1lem2  24876  chebbnd1lem3  24877  chtppilimlem1  24879  chpchtlim  24885  vmadivsum  24888  vmadivsumb  24889  rpvmasumlem  24893  dchrisumlem2  24896  dchrmusum2  24900  dchrvmasumlem2  24904  dchrvmasumlem3  24905  dchrisum0flblem2  24915  dchrisum0fno1  24917  dchrisum0re  24919  dchrisum0lem1  24922  dchrisum0lem2a  24923  mudivsum  24936  mulogsumlem  24937  mulog2sumlem2  24941  vmalogdivsum2  24944  selberglem2  24952  selbergb  24955  selberg2b  24958  logdivbnd  24962  selberg3lem1  24963  selberg3lem2  24964  selberg4lem1  24966  pntrmax  24970  pntrlog2bndlem2  24984  pntrlog2bndlem3  24985  pntrlog2bndlem5  24987  pntrlog2bndlem6a  24988  pntrlog2bndlem6  24989  pntrlog2bnd  24990  pntpbnd1a  24991  pntpbnd1  24992  pntpbnd2  24993  pntibndlem1  24995  pntibndlem2  24997  pntlemb  25003  pntlemq  25007  pntlemr  25008  pntlemj  25009  pntlemk  25012  qabvle  25031  padicabvcxp  25038  ostth2lem2  25040  ostth2lem3  25041  ostth2lem4  25042  ostth3  25044  legtrid  25204  legov3  25211  krippenlem  25303  mideulem2  25344  midex  25347  opphllem5  25361  opphllem6  25362  opphl  25364  lmieu  25394  lmiisolem  25406  ttgcontlem1  25483  colinearalglem4  25507  axpaschlem  25538  axcontlem7  25568  clwlkndivn  26146  nvge0  26707  smcnlem  26737  nmoub3i  26818  nmoub2i  26819  nmlno0lem  26838  minvecolem2  26921  htthlem  26964  norm3dif2  27198  bcs2  27229  chscllem2  27687  eigposi  27885  nmopub2tALT  27958  nmfnleub2  27975  nmlnop0iALT  28044  riesz1  28114  cnlnadjlem2  28117  nmopcoadji  28150  leopsq  28178  leopmul  28183  leopnmid  28187  nmopleid  28188  opsqrlem6  28194  0leopj  28235  hstle1  28275  strlem3a  28301  mdslmd4i  28382  cvexchlem  28417  cdj1i  28482  le2halvesd  28716  xlt2addrd  28719  2sqcoprm  28784  2sqmod  28785  archiabllem1a  28882  archiabllem2a  28885  archiabllem2c  28886  xrge0tsmsd  28922  orngsqr  28941  ornglmulle  28942  orngrmulle  28943  orng0le1  28949  fzto1st1  28989  metideq  29070  metider  29071  sqsscirc1  29088  esummono  29249  esumpad2  29251  esumle  29253  esumlef  29257  esumcst  29258  esumrnmpt2  29263  esum2d  29288  aean  29440  dya2ub  29465  dya2icoseg  29472  omssubadd  29495  inelcarsg  29506  carsgsigalem  29510  carsggect  29513  carsgclctunlem2  29514  eulerpartlemb  29563  fibp1  29596  sgnmulsgp  29745  signsplypnf  29759  signsply0  29760  subfacval3  30231  sconpht2  30280  sconpi1  30281  rescon  30288  snmlff  30371  sinccvglem  30626  faclimlem2  30689  btwnouttr2  31105  dnibndlem5  31448  dnibndlem7  31450  dnibndlem8  31451  dnibndlem9  31452  dnibndlem10  31453  dnibnd  31457  knoppcnlem4  31462  knoppcnlem9  31467  unbdqndv2lem1  31476  unbdqndv2lem2  31477  knoppndvlem11  31489  knoppndvlem12  31490  knoppndvlem14  31492  knoppndvlem15  31493  knoppndvlem17  31495  knoppndvlem18  31496  knoppndvlem19  31497  knoppndvlem21  31499  ltflcei  32363  poimirlem9  32384  poimirlem26  32401  poimirlem27  32402  poimirlem29  32404  heicant  32410  mblfinlem2  32413  mblfinlem3  32414  mblfinlem4  32415  volsupnfl  32420  itg2addnclem  32427  itg2addnclem3  32429  iblmulc2nc  32441  bddiblnc  32446  ftc1cnnclem  32449  ftc1anclem6  32456  ftc1anclem7  32457  ftc1anclem8  32458  ftc2nc  32460  dvasin  32462  geomcau  32521  bfplem2  32588  rrncmslem  32597  rrnequiv  32600  lsatcvatlem  33150  islshpcv  33154  atlatmstc  33420  cvlsupr7  33449  cvrval3  33513  cvrval5  33515  cvrexchlem  33519  atcvrj1  33531  cvrat3  33542  cvrat4  33543  atbtwn  33546  1cvratex  33573  hlatexch4  33581  3atlem1  33583  3atlem2  33584  atcvrlln2  33619  atcvrlln  33620  lplnllnneN  33656  llncvrlpln2  33657  4atlem3b  33698  lplncvrlvol2  33715  dalemswapyz  33756  dalemswapyzps  33790  dalem25  33798  dalem39  33811  dalem58  33830  dalem59  33831  lneq2at  33878  lncvrat  33882  dalawlem2  33972  dalawlem3  33973  dalawlem4  33974  dalawlem6  33976  dalawlem9  33979  dalawlem11  33981  dalawlem12  33982  lhpocnle  34116  lhpmcvr3  34125  lhpmcvr5N  34127  lhpmcvr6N  34128  4atexlemunv  34166  4atexlemc  34169  4atexlemex2  34171  lautm  34194  cdlemc2  34293  cdleme5  34341  cdleme11j  34368  cdleme16b  34380  cdlemednpq  34400  cdleme19e  34409  cdleme20i  34419  cdleme22a  34442  cdleme22cN  34444  cdleme22d  34445  cdleme22e  34446  cdleme22eALTN  34447  cdleme22f  34448  cdleme23c  34453  cdleme30a  34480  cdleme35a  34550  cdleme35b  34552  cdleme42h  34584  cdlemeg46rgv  34630  cdlemg8b  34730  cdlemg12e  34749  cdlemg13a  34753  cdlemg17pq  34774  cdlemg18c  34782  cdlemg19  34786  cdlemg21  34788  cdlemg31d  34802  cdlemg33a  34808  tendoid  34875  cdlemk4  34936  cdlemki  34943  cdlemk10  34945  cdlemksv2  34949  cdlemk12  34952  cdlemk14  34956  cdlemk15  34957  cdlemk1u  34961  cdlemk5u  34963  cdlemk12u  34974  cdlemk45  35049  cdlemk48  35052  dia2dimlem1  35167  dia2dimlem2  35168  dia2dimlem3  35169  cdlemm10N  35221  cdlemn2  35298  dihjustlem  35319  dihglbcpreN  35403  dihmeetlem3N  35408  irrapxlem1  36200  pell1qrgaplem  36251  pell1qrgap  36252  monotoddzzfi  36321  jm2.24nn  36340  congtr  36346  congmul  36348  congsub  36351  fzmaxdif  36362  acongeq  36364  jm2.20nn  36378  jm2.25  36380  hbtlem4  36511  dgrsub2  36520  mpaaeu  36535  idomsubgmo  36591  int-sqgeq0d  37307  int-ineqmvtd  37312  cvgdvgrat  37330  radcnvrat  37331  hashnzfzclim  37339  dvconstbi  37351  binomcxplemdvbinom  37370  isosctrlem1ALT  37988  mulltgt0  38000  oddfl  38226  2timesgt  38237  lt3addmuld  38252  lt4addmuld  38257  supxrgere  38287  supxrgelem  38291  supxrge  38292  xadd0ge2  38295  infrpge  38305  xrlexaddrp  38306  xralrple2  38308  infxr  38321  infleinflem1  38324  infleinflem2  38325  infleinf  38326  xralrple4  38327  xralrple3  38328  recnnltrp  38331  rpgtrecnn  38335  xrralrecnnge  38351  iccshift  38388  iooshift  38392  ressiocsup  38425  ressioosup  38426  fsumnncl  38435  fmul01  38444  fmul01lt1lem1  38448  fmul01lt1lem2  38449  mccllem  38461  climrec  38467  climexp  38469  climneg  38474  limcrecl  38493  sumnnodd  38494  lptioo2  38495  lptioo1  38496  ltmod  38502  lptre2pt  38504  0ellimcdiv  38513  limclner  38515  fnlimcnv  38531  cncficcgt0  38571  cncfioobdlem  38579  ioodvbdlimc1lem1  38618  ioodvbdlimc1lem2  38619  ioodvbdlimc2lem  38621  dvdsn1add  38626  dvnxpaek  38629  dvnmul  38630  dvnprodlem1  38633  itgiccshift  38669  itgperiod  38670  sublevolico  38674  ismbl3  38676  ovolsplit  38678  ismbl4  38683  stoweidlem1  38691  stoweidlem11  38701  stoweidlem13  38703  stoweidlem26  38716  stoweidlem34  38724  stoweidlem38  38728  stoweidlem42  38732  stoweidlem51  38741  stoweidlem59  38749  stirlinglem5  38768  stirlinglem6  38769  stirlinglem7  38770  stirlinglem10  38773  stirlinglem11  38774  stirlinglem13  38776  stirlinglem15  38778  dirkercncflem1  38793  dirkercncflem4  38796  fourierdlem4  38801  fourierdlem10  38807  fourierdlem11  38808  fourierdlem15  38812  fourierdlem20  38817  fourierdlem25  38822  fourierdlem26  38823  fourierdlem30  38827  fourierdlem37  38834  fourierdlem39  38836  fourierdlem40  38837  fourierdlem41  38838  fourierdlem42  38839  fourierdlem44  38841  fourierdlem47  38843  fourierdlem48  38844  fourierdlem49  38845  fourierdlem50  38846  fourierdlem51  38847  fourierdlem52  38848  fourierdlem54  38850  fourierdlem60  38856  fourierdlem61  38857  fourierdlem63  38859  fourierdlem64  38860  fourierdlem65  38861  fourierdlem73  38869  fourierdlem74  38870  fourierdlem75  38871  fourierdlem76  38872  fourierdlem78  38874  fourierdlem79  38875  fourierdlem81  38877  fourierdlem84  38880  fourierdlem87  38883  fourierdlem92  38888  fourierdlem93  38889  fourierdlem101  38897  fourierdlem102  38898  fourierdlem103  38899  fourierdlem104  38900  fourierdlem111  38907  fourierdlem114  38910  sqwvfoura  38918  sqwvfourb  38919  fouriersw  38921  etransclem19  38943  etransclem23  38947  etransclem24  38948  etransclem25  38949  etransclem27  38951  etransclem32  38956  etransclem35  38959  etransclem48  38972  qndenserrnbllem  38987  ioorrnopnlem  38997  ioorrnopnxrlem  38999  fsumlesge0  39067  sge0cl  39071  sge0supre  39079  sge0less  39082  sge0gerp  39085  sge0ltfirp  39090  sge0le  39097  sge0ltfirpmpt  39098  sge0split  39099  sge0rpcpnf  39111  sge0ltfirpmpt2  39116  sge0isum  39117  sge0xaddlem1  39123  sge0pnffigtmpt  39130  sge0pnffsumgt  39132  sge0gtfsumgt  39133  sge0seq  39136  nnfoctbdjlem  39145  meassle  39153  meaiuninclem  39170  meaiininclem  39173  omeiunle  39204  omeiunltfirp  39206  carageniuncllem2  39209  carageniuncl  39210  omess0  39221  hoicvr  39235  ovnlerp  39249  ovnsubaddlem1  39257  hsphoidmvle2  39272  hoidmv1lelem2  39279  hoidmv1le  39281  hoidmvlelem1  39282  hoidmvlelem2  39283  hoidmvlelem3  39284  hoidmvlelem5  39286  ovnhoilem2  39289  ovnhoi  39290  hoidifhspdmvle  39307  hoiqssbllem2  39310  hspmbllem2  39314  hspmbllem3  39315  hspmbl  39316  vonioolem2  39369  vonicclem2  39372  smfaddlem1  39446  smflimlem2  39455  smflimlem4  39457  smfmullem1  39473  perfectALTVlem2  39963  nbfusgrlevtxm2  40601  clwlksndivn  41274  eucrct2eupth  41408  frgrwopreglem2  41477  nnpw2blen  42167
  Copyright terms: Public domain W3C validator