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

Theorem breqtrd 5083
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 5069 . 2 (𝜑 → (𝐴𝑅𝐵𝐴𝑅𝐶))
41, 3mpbid 233 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528   class class class wbr 5057
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-br 5058
This theorem is referenced by:  breqtrrd  5085  breqtrid  5094  domunsn  8655  mapdom2  8676  phplem4  8687  mapfien2  8860  wemaplem2  8999  infdifsn  9108  cantnff  9125  infxpenlem  9427  infmap2  9628  ssfin4  9720  canthp1lem1  10062  nqereq  10345  ltexnq  10385  ltbtwnnq  10388  add20  11140  mullt0  11147  ltm1  11470  recgt0  11474  prodgt0  11475  ltmul1a  11477  mulge0b  11498  recp1lt1  11526  recreclt  11527  ledivp1  11530  ledivp1i  11553  ltdivp1i  11554  eluzmn  12238  ltaddrp2d  12453  mul2lt0bi  12483  prodge0rd  12484  xleadd1a  12634  xov1plusxeqvd  12872  fz01en  12923  fzonmapblen  13071  fladdz  13183  flhalf  13188  fldiv  13216  modsubdir  13296  fzen2  13325  serle  13413  ltexp2a  13518  leexp2a  13524  exple1  13528  expubnd  13529  bernneq  13578  expmulnbnd  13584  discr1  13588  discr  13589  faclbnd6  13647  hashfz  13776  hashfun  13786  seqcoll  13810  sqeqd  14513  sqrlem7  14596  sqrtge0  14605  sqrtneglem  14614  abslt  14662  absle  14663  abstri  14678  rlimge0  14926  reccn2  14941  climaddc2  14980  isercolllem1  15009  caucvgrlem  15017  summolem2a  15060  isumge0  15109  fsumle  15142  fsumlt  15143  o1fsum  15156  supcvg  15199  expcnv  15207  geolim  15214  geolim2  15215  georeclim  15216  geo2lim  15219  mertenslem1  15228  mertens  15230  prodmolem2a  15276  efcllem  15419  ef0lem  15420  efgt0  15444  eftlub  15450  eflt  15458  sinbnd  15521  cosbnd  15522  ef01bndlem  15525  sin01gt0  15531  cos01gt0  15532  sin02gt0  15533  eirrlem  15545  rpnnen2lem11  15565  rpnnen2lem12  15566  ruclem11  15581  dvdssub2  15639  dvdsadd2b  15644  dvdsexp  15665  3dvds  15668  opoe  15700  bitsfzolem  15771  bitsinv1lem  15778  bezoutlem4  15878  dvdsgcd  15880  dvdsmulgcd  15893  bezoutr1  15901  nn0seqcvgd  15902  rpmulgcd2  15988  qredeq  15989  rpdvds  15992  prmind2  16017  divdenle  16077  hashdvds  16100  phimullem  16104  eulerthlem2  16107  prmdiveq  16111  prmdivdiv  16112  pythagtriplem4  16144  pythagtriplem10  16145  pythagtriplem19  16158  iserodd  16160  pcpre1  16167  pcadd2  16214  qexpz  16225  expnprm  16226  oddprmdvds  16227  pockthlem  16229  prmreclem2  16241  prmreclem3  16242  4sqlem7  16268  4sqlem10  16271  4sqlem11  16279  4sqlem12  16280  4sqlem14  16282  4sqlem15  16283  4sqlem16  16284  0ram  16344  ffthiso  17187  latmlej12  17689  qusgrp  18273  pgpfi1  18649  sylow1lem4  18655  sylow1lem5  18656  odcau  18658  pgpfi  18659  pgpssslw  18668  sylow3lem4  18684  sylow3lem6  18686  efgsfo  18794  frgp0  18815  odadd1  18897  odadd2  18898  odadd  18899  gexexlem  18901  lt6abl  18944  gsumzsubmcl  18967  pwsgsum  19031  dprd2dlem1  19092  dprd2d2  19095  ablfacrplem  19116  ablfacrp  19117  ablfacrp2  19118  ablfac1b  19121  ablfac1eu  19124  pgpfac1lem3a  19127  ablfaclem2  19137  dvdsrid  19330  dvdsrtr  19331  dvdsrneg  19333  unitmulcl  19343  unitgrp  19346  unitnegcl  19360  isdrng2  19441  subrguss  19479  subrgunit  19482  abvsubtri  19535  fidomndrnglem  20007  psrbaglesupp  20076  gzrngunit  20539  prmirredlem  20568  znidomb  20636  frlmgsum  20844  invrvald  21213  psmetsym  22847  psmettri  22848  mettri2  22878  xmetsym  22884  xmettri  22888  prdsxmetlem  22905  xblss2ps  22938  xblss2  22939  blhalf  22942  xmsge0  23000  ngptgp  23172  nrginvrcnlem  23227  nmoeq0  23272  cnmet  23307  blcvx  23333  opnreen  23366  metdcnlem  23371  metdstri  23386  metdsle  23387  metnrmlem1  23394  metnrmlem3  23396  lebnumlem1  23492  pi1inv  23583  cphnmf  23726  ipge0  23729  ipcau2  23764  tcphcphlem1  23765  csbren  23929  minveclem2  23956  minveclem3  23959  ovolssnul  24015  ovolctb  24018  ovolunnul  24028  ovoliunlem1  24030  ovoliun2  24034  ovoliunnul  24035  ioombl1lem4  24089  uniioombllem3  24113  uniioombllem4  24114  uniioombllem5  24115  uniioombl  24117  volcn  24134  vitalilem2  24137  vitalilem5  24140  itg1lea  24240  mbfi1fseqlem6  24248  mbfi1flimlem  24250  itg2eqa  24273  itg2splitlem  24276  itg2split  24277  itg2monolem1  24278  itg2cnlem2  24290  iblabsr  24357  iblmulc2  24358  dveflem  24503  dvef  24504  dvferm2lem  24510  dvlip  24517  c1liplem1  24520  dveq0  24524  dvlt0  24529  dvivthlem1  24532  lhop1  24538  dvfsumle  24545  dvfsumlem4  24553  dvfsumrlim3  24557  dvfsum2  24558  ftc1a  24561  ftc1lem4  24563  deg1add  24624  ply1divex  24657  ply1rem  24684  fta1glem2  24687  fta1blem  24689  ig1pdvds  24697  plyeq0lem  24727  dgrcolem2  24791  plydivlem4  24812  plyrem  24821  fta1lem  24823  aalioulem3  24850  aaliou2b  24857  aaliou3lem3  24860  aaliou3lem8  24861  ulmcn  24914  ulmdvlem1  24915  itgulm  24923  pserulm  24937  pserdvlem2  24943  abelthlem2  24947  abelthlem5  24950  abelthlem6  24951  abelthlem7  24953  abelthlem8  24954  abelthlem9  24955  sinq12gt0  25020  sinq34lt0t  25022  cosq14gt0  25023  cosq14ge0  25024  cos02pilt1  25038  efif1olem3  25055  argimgt0  25122  argimlt0  25123  logneg2  25125  logcnlem3  25154  logcnlem4  25155  logtayllem  25169  logtayl2  25172  cxpsqrtlem  25212  cxpsqrt  25213  cxpaddlelem  25259  abscxpbnd  25261  loglesqrt  25266  ang180lem2  25315  atanlogaddlem  25418  atanlogsublem  25420  atantan  25428  atans2  25436  atantayl  25442  leibpi  25447  log2tlbnd  25450  birthdaylem2  25457  birthdaylem3  25458  cxp2limlem  25480  jensenlem2  25492  jensen  25493  logdiflbnd  25499  emcllem2  25501  emcllem4  25503  harmonicbnd4  25515  fsumharmonic  25516  lgamgulmlem2  25534  lgamgulm2  25540  lgambdd  25541  lgamucov  25542  lgamcvglem  25544  lgamcvg2  25559  gamcvg  25560  wilthlem3  25574  basellem1  25585  basellem3  25587  basellem4  25588  fsumdvdsdiaglem  25687  dvdsppwf1o  25690  dvdsmulf1o  25698  chteq0  25712  chtub  25715  chpub  25723  logfacubnd  25724  logfaclbnd  25725  logexprlim  25728  perfectlem2  25733  dchrfi  25758  bclbnd  25783  bposlem1  25787  bposlem3  25789  bposlem4  25790  bposlem6  25792  lgslem1  25800  lgsqrlem2  25850  lgsqrlem4  25852  lgseisenlem2  25879  lgsquadlem1  25883  lgsquadlem2  25884  lgsquad2lem1  25887  2sqlem3  25923  2sqlem4  25924  2sqlem8  25929  2sqlem11  25932  2sqcoprm  25938  2sqmod  25939  chebbnd1lem2  25973  chebbnd1lem3  25974  chtppilimlem1  25976  chpchtlim  25982  vmadivsum  25985  vmadivsumb  25986  rpvmasumlem  25990  dchrisumlem2  25993  dchrmusum2  25997  dchrvmasumlem2  26001  dchrvmasumlem3  26002  dchrisum0flblem2  26012  dchrisum0fno1  26014  dchrisum0re  26016  dchrisum0lem1  26019  dchrisum0lem2a  26020  mudivsum  26033  mulogsumlem  26034  mulog2sumlem2  26038  vmalogdivsum2  26041  selberglem2  26049  selbergb  26052  selberg2b  26055  logdivbnd  26059  selberg3lem1  26060  selberg3lem2  26061  selberg4lem1  26063  pntrmax  26067  pntrlog2bndlem2  26081  pntrlog2bndlem3  26082  pntrlog2bndlem5  26084  pntrlog2bndlem6a  26085  pntrlog2bndlem6  26086  pntrlog2bnd  26087  pntpbnd1a  26088  pntpbnd1  26089  pntpbnd2  26090  pntibndlem1  26092  pntibndlem2  26094  pntlemb  26100  pntlemq  26104  pntlemr  26105  pntlemj  26106  pntlemk  26109  qabvle  26128  padicabvcxp  26135  ostth2lem2  26137  ostth2lem3  26138  ostth2lem4  26139  ostth3  26141  legtrid  26304  legov3  26311  krippenlem  26403  mideulem2  26447  midex  26450  opphllem5  26464  opphllem6  26465  opphl  26467  lmieu  26497  lmiisolem  26509  ttgcontlem1  26598  colinearalglem4  26622  axpaschlem  26653  axcontlem7  26683  nbfusgrlevtxm2  27087  clwlksndivn  27792  eucrct2eupth  27951  nvge0  28377  smcnlem  28401  nmoub3i  28477  nmoub2i  28478  nmlno0lem  28497  minvecolem2  28579  htthlem  28621  norm3dif2  28855  bcs2  28886  chscllem2  29342  eigposi  29540  nmopub2tALT  29613  nmfnleub2  29630  nmlnop0iALT  29699  riesz1  29769  cnlnadjlem2  29772  nmopcoadji  29805  leopsq  29833  leopmul  29838  leopnmid  29842  nmopleid  29843  opsqrlem6  29849  0leopj  29890  hstle1  29930  strlem3a  29956  mdslmd4i  30037  cvexchlem  30072  cdj1i  30137  unidifsnel  30222  unidifsnne  30223  le2halvesd  30405  xlt2addrd  30408  fsumub  30471  wrdt2ind  30554  xrge0tsmsd  30619  fzto1st1  30671  cycpmco2lem4  30698  cycpmco2lem6  30700  cyc3conja  30726  archiabllem1a  30747  archiabllem2a  30750  archiabllem2c  30751  orngsqr  30804  ornglmulle  30805  orngrmulle  30806  orng0le1  30812  fedgmullem1  30924  fedgmullem2  30925  metideq  31032  metider  31033  sqsscirc1  31050  esummono  31212  esumpad2  31214  esumle  31216  esumlef  31220  esumcst  31221  esumrnmpt2  31226  esum2d  31251  aean  31402  dya2ub  31427  dya2icoseg  31434  omssubadd  31457  inelcarsg  31468  carsgsigalem  31472  carsggect  31475  carsgclctunlem2  31476  eulerpartlemb  31525  fibp1  31558  sgnmulsgp  31707  signsplypnf  31719  signsply0  31720  fdvposlt  31769  fdvposle  31771  reprgt  31791  logdivsqrle  31820  hgt750lemb  31826  hgt750leme  31828  tgoldbachgtde  31830  subfacval3  32333  sconnpht2  32382  sconnpi1  32383  resconn  32390  snmlff  32473  sinccvglem  32812  faclimlem2  32873  btwnouttr2  33380  dnibndlem5  33718  dnibndlem7  33720  dnibndlem8  33721  dnibndlem9  33722  dnibndlem10  33723  dnibnd  33727  knoppcnlem4  33732  knoppcnlem9  33737  unbdqndv2lem1  33745  unbdqndv2lem2  33746  knoppndvlem11  33758  knoppndvlem12  33759  knoppndvlem14  33761  knoppndvlem15  33762  knoppndvlem17  33764  knoppndvlem18  33765  knoppndvlem19  33766  knoppndvlem21  33768  ltflcei  34761  poimirlem9  34782  poimirlem26  34799  poimirlem27  34800  poimirlem29  34802  heicant  34808  mblfinlem2  34811  mblfinlem3  34812  mblfinlem4  34813  volsupnfl  34818  itg2addnclem  34824  itg2addnclem3  34826  iblmulc2nc  34838  bddiblnc  34843  ftc1cnnclem  34846  ftc1anclem6  34853  ftc1anclem7  34854  ftc1anclem8  34855  ftc2nc  34857  dvasin  34859  geomcau  34915  bfplem2  34982  rrncmslem  34991  rrnequiv  34994  lsatcvatlem  36065  islshpcv  36069  atlatmstc  36335  cvlsupr7  36364  cvrval3  36429  cvrval5  36431  cvrexchlem  36435  atcvrj1  36447  cvrat3  36458  cvrat4  36459  atbtwn  36462  1cvratex  36489  hlatexch4  36497  3atlem1  36499  3atlem2  36500  atcvrlln2  36535  atcvrlln  36536  lplnllnneN  36572  llncvrlpln2  36573  4atlem3b  36614  lplncvrlvol2  36631  dalemswapyz  36672  dalemswapyzps  36706  dalem25  36714  dalem39  36727  dalem58  36746  dalem59  36747  lneq2at  36794  lncvrat  36798  dalawlem2  36888  dalawlem3  36889  dalawlem4  36890  dalawlem6  36892  dalawlem9  36895  dalawlem11  36897  dalawlem12  36898  lhpocnle  37032  lhpmcvr3  37041  lhpmcvr5N  37043  lhpmcvr6N  37044  4atexlemunv  37082  4atexlemc  37085  4atexlemex2  37087  lautm  37110  cdlemc2  37208  cdleme5  37256  cdleme11j  37283  cdleme16b  37295  cdlemednpq  37315  cdleme19e  37323  cdleme20i  37333  cdleme22a  37356  cdleme22cN  37358  cdleme22d  37359  cdleme22e  37360  cdleme22eALTN  37361  cdleme22f  37362  cdleme23c  37367  cdleme30a  37394  cdleme35a  37464  cdleme35b  37466  cdleme42h  37498  cdlemeg46rgv  37544  cdlemg8b  37644  cdlemg12e  37663  cdlemg13a  37667  cdlemg17pq  37688  cdlemg18c  37696  cdlemg19  37700  cdlemg21  37702  cdlemg31d  37716  cdlemg33a  37722  tendoid  37789  cdlemk4  37850  cdlemki  37857  cdlemk10  37859  cdlemksv2  37863  cdlemk12  37866  cdlemk14  37870  cdlemk15  37871  cdlemk1u  37875  cdlemk5u  37877  cdlemk12u  37888  cdlemk45  37963  cdlemk48  37966  dia2dimlem1  38080  dia2dimlem2  38081  dia2dimlem3  38082  cdlemm10N  38134  cdlemn2  38211  dihjustlem  38232  dihglbcpreN  38316  dihmeetlem3N  38321  zrtdvds  39071  rtprmirr  39072  dffltz  39149  fltnlta  39153  irrapxlem1  39297  pell1qrgaplem  39348  pell1qrgap  39349  monotoddzzfi  39417  jm2.24nn  39434  congtr  39440  congmul  39442  congsub  39445  fzmaxdif  39456  acongeq  39458  jm2.20nn  39472  jm2.25  39474  hbtlem4  39604  dgrsub2  39613  mpaaeu  39628  idomsubgmo  39676  iscard4  39778  leeq2d  40386  int-sqgeq0d  40417  int-ineqmvtd  40422  cvgdvgrat  40522  radcnvrat  40523  hashnzfzclim  40531  dvconstbi  40543  binomcxplemdvbinom  40562  isosctrlem1ALT  41145  mulltgt0  41156  rnmptbd2lem  41396  oddfl  41419  2timesgt  41430  lt3addmuld  41444  lt4addmuld  41449  supxrgere  41477  supxrgelem  41481  supxrge  41482  xadd0ge2  41485  infrpge  41495  xrlexaddrp  41496  xralrple2  41498  infxr  41511  infleinflem1  41514  infleinflem2  41515  infleinf  41516  xralrple4  41517  xralrple3  41518  recnnltrp  41521  rpgtrecnn  41525  xrralrecnnge  41538  rexabslelem  41568  infrnmptle  41573  supminfxr  41616  xrpnf  41638  iccshift  41670  iooshift  41674  ressiocsup  41706  ressioosup  41707  fsumnncl  41728  fmul01  41737  fmul01lt1lem1  41741  fmul01lt1lem2  41742  mccllem  41754  climrec  41760  climexp  41762  climneg  41767  limcrecl  41786  sumnnodd  41787  lptioo2  41788  lptioo1  41789  ltmod  41795  lptre2pt  41797  0ellimcdiv  41806  limclner  41808  fnlimcnv  41824  climinf2lem  41863  limsupubuzlem  41869  limsup10exlem  41929  limsupgtlem  41934  dfxlim2v  42004  xlimliminflimsup  42019  cncficcgt0  42047  cncfioobdlem  42055  ioodvbdlimc1lem1  42092  ioodvbdlimc1lem2  42093  ioodvbdlimc2lem  42095  dvdsn1add  42100  dvnxpaek  42103  dvnmul  42104  dvnprodlem1  42107  itgiccshift  42141  itgperiod  42142  sublevolico  42146  ismbl3  42148  ovolsplit  42150  ismbl4  42155  stoweidlem1  42163  stoweidlem11  42173  stoweidlem13  42175  stoweidlem26  42188  stoweidlem34  42196  stoweidlem38  42200  stoweidlem42  42204  stoweidlem51  42213  stoweidlem59  42221  stirlinglem5  42240  stirlinglem6  42241  stirlinglem7  42242  stirlinglem10  42245  stirlinglem11  42246  stirlinglem13  42248  stirlinglem15  42250  dirkercncflem1  42265  dirkercncflem4  42268  fourierdlem4  42273  fourierdlem10  42279  fourierdlem11  42280  fourierdlem15  42284  fourierdlem20  42289  fourierdlem25  42294  fourierdlem26  42295  fourierdlem30  42299  fourierdlem37  42306  fourierdlem39  42308  fourierdlem40  42309  fourierdlem41  42310  fourierdlem42  42311  fourierdlem44  42313  fourierdlem47  42315  fourierdlem48  42316  fourierdlem49  42317  fourierdlem50  42318  fourierdlem51  42319  fourierdlem52  42320  fourierdlem54  42322  fourierdlem60  42328  fourierdlem61  42329  fourierdlem63  42331  fourierdlem64  42332  fourierdlem65  42333  fourierdlem73  42341  fourierdlem74  42342  fourierdlem75  42343  fourierdlem76  42344  fourierdlem78  42346  fourierdlem79  42347  fourierdlem81  42349  fourierdlem84  42352  fourierdlem87  42355  fourierdlem92  42360  fourierdlem93  42361  fourierdlem101  42369  fourierdlem102  42370  fourierdlem103  42371  fourierdlem104  42372  fourierdlem111  42379  fourierdlem114  42382  sqwvfoura  42390  sqwvfourb  42391  fouriersw  42393  etransclem19  42415  etransclem23  42419  etransclem24  42420  etransclem25  42421  etransclem27  42423  etransclem32  42428  etransclem35  42431  etransclem48  42444  qndenserrnbllem  42456  ioorrnopnlem  42466  ioorrnopnxrlem  42468  fsumlesge0  42536  sge0cl  42540  sge0supre  42548  sge0less  42551  sge0gerp  42554  sge0ltfirp  42559  sge0le  42566  sge0ltfirpmpt  42567  sge0split  42568  sge0rpcpnf  42580  sge0ltfirpmpt2  42585  sge0isum  42586  sge0xaddlem1  42592  sge0pnffigtmpt  42599  sge0pnffsumgt  42601  sge0gtfsumgt  42602  sge0seq  42605  nnfoctbdjlem  42614  meassle  42622  meaiuninclem  42639  meaiininclem  42645  omeiunle  42676  omeiunltfirp  42678  carageniuncllem2  42681  carageniuncl  42682  omess0  42693  hoicvr  42707  ovnlerp  42721  ovnsubaddlem1  42729  hsphoidmvle2  42744  hoidmv1lelem2  42751  hoidmv1le  42753  hoidmvlelem1  42754  hoidmvlelem2  42755  hoidmvlelem3  42756  hoidmvlelem5  42758  ovnhoilem2  42761  ovnhoi  42762  hoidifhspdmvle  42779  hoiqssbllem2  42782  hspmbllem2  42786  hspmbllem3  42787  hspmbl  42788  vonioolem2  42840  vonicclem2  42843  smfaddlem1  42916  smflimlem2  42925  smflimlem4  42927  smfmullem1  42943  smfinflem  42968  smflimsuplem4  42974  smflimsuplem8  42978  perfectALTVlem2  43764  nnpw2blen  44568  itscnhlinecirc02plem1  44697
  Copyright terms: Public domain W3C validator