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

Theorem breqtrd 4881
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 4867 . 2 (𝜑 → (𝐴𝑅𝐵𝐴𝑅𝐶))
41, 3mpbid 223 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637   class class class wbr 4855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-rab 3116  df-v 3404  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-br 4856
This theorem is referenced by:  breqtrrd  4883  syl5breq  4892  domunsn  8358  mapdom2  8379  phplem4  8390  mapfien2  8562  wemaplem2  8700  infdifsn  8810  cantnff  8827  infxpenlem  9128  pwcda1  9310  pwcdadom  9332  infmap2  9334  ackbij1lem5  9340  ssfin4  9426  canthp1lem1  9768  nqereq  10051  ltexnq  10091  ltbtwnnq  10094  add20  10834  mullt0  10841  ltm1  11157  recgt0  11161  prodgt0  11162  prodge0OLD  11164  ltmul1a  11166  mulge0b  11187  recp1lt1  11215  recreclt  11216  ledivp1  11219  ledivp1i  11243  ltdivp1i  11244  eluzmn  11930  ltaddrp2d  12139  mul2lt0bi  12169  prodge0rd  12170  xleadd1a  12320  xov1plusxeqvd  12560  fz01en  12611  fzonmapblen  12757  fladdz  12869  flhalf  12874  fldiv  12902  modsubdir  12982  fzen2  13011  serle  13098  ltexp2a  13154  leexp2a  13158  exple1  13162  expubnd  13163  bernneq  13232  expmulnbnd  13238  discr1  13242  discr  13243  faclbnd6  13325  hashfz  13450  hashfun  13460  seqcoll  13484  sqeqd  14148  sqrlem7  14231  sqrtge0  14240  sqrtneglem  14249  abslt  14296  absle  14297  abstri  14312  rlimge0  14554  reccn2  14569  climaddc2  14608  isercolllem1  14637  caucvgrlem  14645  summolem2a  14688  isumge0  14739  fsumle  14772  fsumlt  14773  o1fsum  14786  supcvg  14829  expcnv  14837  geolim  14842  geolim2  14843  georeclim  14844  geo2lim  14847  mertenslem1  14856  mertens  14858  prodmolem2a  14904  efcllem  15047  ef0lem  15048  efgt0  15072  eftlub  15078  eflt  15086  sinbnd  15149  cosbnd  15150  ef01bndlem  15153  sin01gt0  15159  cos01gt0  15160  sin02gt0  15161  eirrlem  15171  rpnnen2lem11  15192  rpnnen2lem12  15193  ruclem11  15208  dvdssub2  15265  dvdsadd2b  15270  dvdsexp  15291  3dvds  15294  opoe  15326  bitsfzolem  15394  bitsinv1lem  15401  bezoutlem4  15497  dvdsgcd  15499  dvdsmulgcd  15512  bezoutr1  15520  nn0seqcvgd  15521  rpmulgcd2  15607  qredeq  15608  rpdvds  15611  prmind2  15635  divdenle  15693  hashdvds  15716  phimullem  15720  eulerthlem2  15723  prmdiveq  15727  prmdivdiv  15728  pythagtriplem4  15760  pythagtriplem10  15761  pythagtriplem19  15774  iserodd  15776  pcpre1  15783  pcadd2  15830  qexpz  15841  expnprm  15842  oddprmdvds  15843  pockthlem  15845  prmreclem2  15857  prmreclem3  15858  4sqlem7  15884  4sqlem10  15887  4sqlem11  15895  4sqlem12  15896  4sqlem14  15898  4sqlem15  15899  4sqlem16  15900  0ram  15960  ffthiso  16812  latmlej12  17315  qusgrp  17870  pgpfi1  18230  sylow1lem4  18236  sylow1lem5  18237  odcau  18239  pgpfi  18240  pgpssslw  18249  sylow3lem4  18265  sylow3lem6  18267  efgsfo  18372  frgp0  18393  odadd1  18471  odadd2  18472  odadd  18473  gexexlem  18475  lt6abl  18516  gsumzsubmcl  18538  pwsgsum  18598  dprd2dlem1  18661  dprd2d2  18664  ablfacrplem  18685  ablfacrp  18686  ablfacrp2  18687  ablfac1b  18690  ablfac1eu  18693  pgpfac1lem3a  18696  ablfaclem2  18706  dvdsrid  18872  dvdsrtr  18873  dvdsrneg  18875  unitmulcl  18885  unitgrp  18888  unitnegcl  18902  isdrng2  18980  subrguss  19018  subrgunit  19021  abvsubtri  19058  fidomndrnglem  19534  psrbaglesupp  19596  gzrngunit  20039  prmirredlem  20068  znidomb  20136  frlmgsum  20341  invrvald  20714  psmetsym  22348  psmettri  22349  mettri2  22379  xmetsym  22385  xmettri  22389  prdsxmetlem  22406  xblss2ps  22439  xblss2  22440  blhalf  22443  xmsge0  22501  ngptgp  22673  nrginvrcnlem  22728  nmoeq0  22773  cnmet  22808  blcvx  22834  opnreen  22867  metdcnlem  22872  metdstri  22887  metdsle  22888  metnrmlem1  22895  metnrmlem3  22897  lebnumlem1  22993  pi1inv  23084  cphnmf  23227  ipge0  23230  ipcau2  23265  tchcphlem1  23266  csbren  23416  minveclem2  23431  minveclem3  23434  ovolssnul  23490  ovolctb  23493  ovolunnul  23503  ovoliunlem1  23505  ovoliun2  23509  ovoliunnul  23510  ioombl1lem4  23564  uniioombllem3  23588  uniioombllem4  23589  uniioombllem5  23590  uniioombl  23592  volcn  23609  vitalilem2  23612  vitalilem5  23615  itg1lea  23715  mbfi1fseqlem6  23723  mbfi1flimlem  23725  itg2eqa  23748  itg2splitlem  23751  itg2split  23752  itg2monolem1  23753  itg2cnlem2  23765  iblabsr  23832  iblmulc2  23833  dveflem  23978  dvef  23979  dvferm2lem  23985  dvlip  23992  c1liplem1  23995  dveq0  23999  dvlt0  24004  dvivthlem1  24007  lhop1  24013  dvfsumle  24020  dvfsumlem4  24028  dvfsumrlim3  24032  dvfsum2  24033  ftc1a  24036  ftc1lem4  24038  deg1add  24099  ply1divex  24132  ply1rem  24159  fta1glem2  24162  fta1blem  24164  ig1pdvds  24172  plyeq0lem  24202  dgrcolem2  24266  plydivlem4  24287  plyrem  24296  fta1lem  24298  aalioulem3  24325  aaliou2b  24332  aaliou3lem3  24335  aaliou3lem8  24336  ulmcn  24389  ulmdvlem1  24390  itgulm  24398  pserulm  24412  pserdvlem2  24418  abelthlem2  24422  abelthlem5  24425  abelthlem6  24426  abelthlem7  24428  abelthlem8  24429  abelthlem9  24430  sinq12gt0  24496  sinq34lt0t  24498  cosq14gt0  24499  cosq14ge0  24500  efif1olem3  24527  argimgt0  24594  argimlt0  24595  logneg2  24597  logcnlem3  24626  logcnlem4  24627  logtayllem  24641  logtayl2  24644  cxpsqrtlem  24684  cxpsqrt  24685  cxpaddlelem  24728  abscxpbnd  24730  loglesqrt  24735  ang180lem2  24776  atanlogaddlem  24876  atanlogsublem  24878  atantan  24886  atans2  24894  atantayl  24900  leibpi  24905  log2tlbnd  24908  birthdaylem2  24915  birthdaylem3  24916  cxp2limlem  24938  jensenlem2  24950  jensen  24951  logdiflbnd  24957  emcllem2  24959  emcllem4  24961  harmonicbnd4  24973  fsumharmonic  24974  lgamgulmlem2  24992  lgamgulm2  24998  lgambdd  24999  lgamucov  25000  lgamcvglem  25002  lgamcvg2  25017  gamcvg  25018  wilthlem3  25032  basellem1  25043  basellem3  25045  basellem4  25046  fsumdvdsdiaglem  25145  dvdsppwf1o  25148  dvdsmulf1o  25156  chteq0  25170  chtub  25173  chpub  25181  logfacubnd  25182  logfaclbnd  25183  logexprlim  25186  perfectlem2  25191  dchrfi  25216  bclbnd  25241  bposlem1  25245  bposlem3  25247  bposlem4  25248  bposlem6  25250  lgslem1  25258  lgsqrlem2  25308  lgsqrlem4  25310  lgseisenlem2  25337  lgsquadlem1  25341  lgsquadlem2  25342  lgsquad2lem1  25345  2sqlem3  25381  2sqlem4  25382  2sqlem8  25387  2sqlem11  25390  chebbnd1lem2  25395  chebbnd1lem3  25396  chtppilimlem1  25398  chpchtlim  25404  vmadivsum  25407  vmadivsumb  25408  rpvmasumlem  25412  dchrisumlem2  25415  dchrmusum2  25419  dchrvmasumlem2  25423  dchrvmasumlem3  25424  dchrisum0flblem2  25434  dchrisum0fno1  25436  dchrisum0re  25438  dchrisum0lem1  25441  dchrisum0lem2a  25442  mudivsum  25455  mulogsumlem  25456  mulog2sumlem2  25460  vmalogdivsum2  25463  selberglem2  25471  selbergb  25474  selberg2b  25477  logdivbnd  25481  selberg3lem1  25482  selberg3lem2  25483  selberg4lem1  25485  pntrmax  25489  pntrlog2bndlem2  25503  pntrlog2bndlem3  25504  pntrlog2bndlem5  25506  pntrlog2bndlem6a  25507  pntrlog2bndlem6  25508  pntrlog2bnd  25509  pntpbnd1a  25510  pntpbnd1  25511  pntpbnd2  25512  pntibndlem1  25514  pntibndlem2  25516  pntlemb  25522  pntlemq  25526  pntlemr  25527  pntlemj  25528  pntlemk  25531  qabvle  25550  padicabvcxp  25557  ostth2lem2  25559  ostth2lem3  25560  ostth2lem4  25561  ostth3  25563  legtrid  25722  legov3  25729  krippenlem  25821  mideulem2  25862  midex  25865  opphllem5  25879  opphllem6  25880  opphl  25882  lmieu  25912  lmiisolem  25924  ttgcontlem1  26001  colinearalglem4  26025  axpaschlem  26056  axcontlem7  26086  nbfusgrlevtxm2  26518  clwlksndivn  27273  eucrct2eupth  27440  nvge0  27878  smcnlem  27902  nmoub3i  27978  nmoub2i  27979  nmlno0lem  27998  minvecolem2  28081  htthlem  28124  norm3dif2  28358  bcs2  28389  chscllem2  28847  eigposi  29045  nmopub2tALT  29118  nmfnleub2  29135  nmlnop0iALT  29204  riesz1  29274  cnlnadjlem2  29277  nmopcoadji  29310  leopsq  29338  leopmul  29343  leopnmid  29347  nmopleid  29348  opsqrlem6  29354  0leopj  29395  hstle1  29435  strlem3a  29461  mdslmd4i  29542  cvexchlem  29577  cdj1i  29642  le2halvesd  29869  xlt2addrd  29872  fsumub  29923  2sqcoprm  29994  2sqmod  29995  archiabllem1a  30092  archiabllem2a  30095  archiabllem2c  30096  xrge0tsmsd  30132  orngsqr  30151  ornglmulle  30152  orngrmulle  30153  orng0le1  30159  fzto1st1  30199  metideq  30283  metider  30284  sqsscirc1  30301  esummono  30463  esumpad2  30465  esumle  30467  esumlef  30471  esumcst  30472  esumrnmpt2  30477  esum2d  30502  aean  30654  dya2ub  30679  dya2icoseg  30686  omssubadd  30709  inelcarsg  30720  carsgsigalem  30724  carsggect  30727  carsgclctunlem2  30728  eulerpartlemb  30777  fibp1  30810  sgnmulsgp  30959  signsplypnf  30974  signsply0  30975  fdvposlt  31024  fdvposle  31026  reprgt  31046  logdivsqrle  31075  hgt750lemb  31081  hgt750leme  31083  tgoldbachgtde  31085  subfacval3  31515  sconnpht2  31564  sconnpi1  31565  resconn  31572  snmlff  31655  sinccvglem  31909  faclimlem2  31973  btwnouttr2  32471  dnibndlem5  32810  dnibndlem7  32812  dnibndlem8  32813  dnibndlem9  32814  dnibndlem10  32815  dnibnd  32819  knoppcnlem4  32824  knoppcnlem9  32829  unbdqndv2lem1  32838  unbdqndv2lem2  32839  knoppndvlem11  32851  knoppndvlem12  32852  knoppndvlem14  32854  knoppndvlem15  32855  knoppndvlem17  32857  knoppndvlem18  32858  knoppndvlem19  32859  knoppndvlem21  32861  ltflcei  33728  poimirlem9  33749  poimirlem26  33766  poimirlem27  33767  poimirlem29  33769  heicant  33775  mblfinlem2  33778  mblfinlem3  33779  mblfinlem4  33780  volsupnfl  33785  itg2addnclem  33791  itg2addnclem3  33793  iblmulc2nc  33805  bddiblnc  33810  ftc1cnnclem  33813  ftc1anclem6  33820  ftc1anclem7  33821  ftc1anclem8  33822  ftc2nc  33824  dvasin  33826  geomcau  33884  bfplem2  33951  rrncmslem  33960  rrnequiv  33963  lsatcvatlem  34847  islshpcv  34851  atlatmstc  35117  cvlsupr7  35146  cvrval3  35211  cvrval5  35213  cvrexchlem  35217  atcvrj1  35229  cvrat3  35240  cvrat4  35241  atbtwn  35244  1cvratex  35271  hlatexch4  35279  3atlem1  35281  3atlem2  35282  atcvrlln2  35317  atcvrlln  35318  lplnllnneN  35354  llncvrlpln2  35355  4atlem3b  35396  lplncvrlvol2  35413  dalemswapyz  35454  dalemswapyzps  35488  dalem25  35496  dalem39  35509  dalem58  35528  dalem59  35529  lneq2at  35576  lncvrat  35580  dalawlem2  35670  dalawlem3  35671  dalawlem4  35672  dalawlem6  35674  dalawlem9  35677  dalawlem11  35679  dalawlem12  35680  lhpocnle  35814  lhpmcvr3  35823  lhpmcvr5N  35825  lhpmcvr6N  35826  4atexlemunv  35864  4atexlemc  35867  4atexlemex2  35869  lautm  35892  cdlemc2  35990  cdleme5  36038  cdleme11j  36065  cdleme16b  36077  cdlemednpq  36097  cdleme19e  36105  cdleme20i  36115  cdleme22a  36138  cdleme22cN  36140  cdleme22d  36141  cdleme22e  36142  cdleme22eALTN  36143  cdleme22f  36144  cdleme23c  36149  cdleme30a  36176  cdleme35a  36246  cdleme35b  36248  cdleme42h  36280  cdlemeg46rgv  36326  cdlemg8b  36426  cdlemg12e  36445  cdlemg13a  36449  cdlemg17pq  36470  cdlemg18c  36478  cdlemg19  36482  cdlemg21  36484  cdlemg31d  36498  cdlemg33a  36504  tendoid  36571  cdlemk4  36632  cdlemki  36639  cdlemk10  36641  cdlemksv2  36645  cdlemk12  36648  cdlemk14  36652  cdlemk15  36653  cdlemk1u  36657  cdlemk5u  36659  cdlemk12u  36670  cdlemk45  36745  cdlemk48  36748  dia2dimlem1  36862  dia2dimlem2  36863  dia2dimlem3  36864  cdlemm10N  36916  cdlemn2  36993  dihjustlem  37014  dihglbcpreN  37098  dihmeetlem3N  37103  irrapxlem1  37905  pell1qrgaplem  37956  pell1qrgap  37957  monotoddzzfi  38025  jm2.24nn  38044  congtr  38050  congmul  38052  congsub  38055  fzmaxdif  38066  acongeq  38068  jm2.20nn  38082  jm2.25  38084  hbtlem4  38214  dgrsub2  38223  mpaaeu  38238  idomsubgmo  38294  leeq2d  38973  int-sqgeq0d  39006  int-ineqmvtd  39011  cvgdvgrat  39029  radcnvrat  39030  hashnzfzclim  39038  dvconstbi  39050  binomcxplemdvbinom  39069  isosctrlem1ALT  39681  mulltgt0  39692  rnmptbd2lem  39963  oddfl  39988  2timesgt  39999  lt3addmuld  40013  lt4addmuld  40018  supxrgere  40046  supxrgelem  40050  supxrge  40051  xadd0ge2  40054  infrpge  40064  xrlexaddrp  40065  xralrple2  40067  infxr  40080  infleinflem1  40083  infleinflem2  40084  infleinf  40085  xralrple4  40086  xralrple3  40087  recnnltrp  40090  rpgtrecnn  40094  xrralrecnnge  40109  rexabslelem  40141  infrnmptle  40146  supminfxr  40190  xrpnf  40212  iccshift  40242  iooshift  40246  ressiocsup  40278  ressioosup  40279  fsumnncl  40300  fmul01  40309  fmul01lt1lem1  40313  fmul01lt1lem2  40314  mccllem  40326  climrec  40332  climexp  40334  climneg  40339  limcrecl  40358  sumnnodd  40359  lptioo2  40360  lptioo1  40361  ltmod  40367  lptre2pt  40369  0ellimcdiv  40378  limclner  40380  fnlimcnv  40396  climinf2lem  40435  limsupubuzlem  40441  limsup10exlem  40501  limsupgtlem  40506  dfxlim2v  40570  cncficcgt0  40598  cncfioobdlem  40606  ioodvbdlimc1lem1  40643  ioodvbdlimc1lem2  40644  ioodvbdlimc2lem  40646  dvdsn1add  40651  dvnxpaek  40654  dvnmul  40655  dvnprodlem1  40658  itgiccshift  40692  itgperiod  40693  sublevolico  40697  ismbl3  40699  ovolsplit  40701  ismbl4  40706  stoweidlem1  40714  stoweidlem11  40724  stoweidlem13  40726  stoweidlem26  40739  stoweidlem34  40747  stoweidlem38  40751  stoweidlem42  40755  stoweidlem51  40764  stoweidlem59  40772  stirlinglem5  40791  stirlinglem6  40792  stirlinglem7  40793  stirlinglem10  40796  stirlinglem11  40797  stirlinglem13  40799  stirlinglem15  40801  dirkercncflem1  40816  dirkercncflem4  40819  fourierdlem4  40824  fourierdlem10  40830  fourierdlem11  40831  fourierdlem15  40835  fourierdlem20  40840  fourierdlem25  40845  fourierdlem26  40846  fourierdlem30  40850  fourierdlem37  40857  fourierdlem39  40859  fourierdlem40  40860  fourierdlem41  40861  fourierdlem42  40862  fourierdlem44  40864  fourierdlem47  40866  fourierdlem48  40867  fourierdlem49  40868  fourierdlem50  40869  fourierdlem51  40870  fourierdlem52  40871  fourierdlem54  40873  fourierdlem60  40879  fourierdlem61  40880  fourierdlem63  40882  fourierdlem64  40883  fourierdlem65  40884  fourierdlem73  40892  fourierdlem74  40893  fourierdlem75  40894  fourierdlem76  40895  fourierdlem78  40897  fourierdlem79  40898  fourierdlem81  40900  fourierdlem84  40903  fourierdlem87  40906  fourierdlem92  40911  fourierdlem93  40912  fourierdlem101  40920  fourierdlem102  40921  fourierdlem103  40922  fourierdlem104  40923  fourierdlem111  40930  fourierdlem114  40933  sqwvfoura  40941  sqwvfourb  40942  fouriersw  40944  etransclem19  40966  etransclem23  40970  etransclem24  40971  etransclem25  40972  etransclem27  40974  etransclem32  40979  etransclem35  40982  etransclem48  40995  qndenserrnbllem  41010  ioorrnopnlem  41020  ioorrnopnxrlem  41022  fsumlesge0  41090  sge0cl  41094  sge0supre  41102  sge0less  41105  sge0gerp  41108  sge0ltfirp  41113  sge0le  41120  sge0ltfirpmpt  41121  sge0split  41122  sge0rpcpnf  41134  sge0ltfirpmpt2  41139  sge0isum  41140  sge0xaddlem1  41146  sge0pnffigtmpt  41153  sge0pnffsumgt  41155  sge0gtfsumgt  41156  sge0seq  41159  nnfoctbdjlem  41168  meassle  41176  meaiuninclem  41193  meaiininclem  41199  omeiunle  41230  omeiunltfirp  41232  carageniuncllem2  41235  carageniuncl  41236  omess0  41247  hoicvr  41261  ovnlerp  41275  ovnsubaddlem1  41283  hsphoidmvle2  41298  hoidmv1lelem2  41305  hoidmv1le  41307  hoidmvlelem1  41308  hoidmvlelem2  41309  hoidmvlelem3  41310  hoidmvlelem5  41312  ovnhoilem2  41315  ovnhoi  41316  hoidifhspdmvle  41333  hoiqssbllem2  41336  hspmbllem2  41340  hspmbllem3  41341  hspmbl  41342  vonioolem2  41394  vonicclem2  41397  smfaddlem1  41470  smflimlem2  41479  smflimlem4  41481  smfmullem1  41497  smfinflem  41522  smflimsuplem4  41528  smflimsuplem8  41532  perfectALTVlem2  42223  nnpw2blen  42959
  Copyright terms: Public domain W3C validator