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

Theorem breqtrrd 4611
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
Hypotheses
Ref Expression
breqtrrd.1 (𝜑𝐴𝑅𝐵)
breqtrrd.2 (𝜑𝐶 = 𝐵)
Assertion
Ref Expression
breqtrrd (𝜑𝐴𝑅𝐶)

Proof of Theorem breqtrrd
StepHypRef Expression
1 breqtrrd.1 . 2 (𝜑𝐴𝑅𝐵)
2 breqtrrd.2 . . 3 (𝜑𝐶 = 𝐵)
32eqcomd 2616 . 2 (𝜑𝐵 = 𝐶)
41, 3breqtrd 4609 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475   class class class wbr 4583
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584
This theorem is referenced by:  marypha1lem  8222  marypha2  8228  unxpwdom  8377  uncdadom  8876  cdacomen  8886  cdaassen  8887  xpcdaen  8888  onacda  8902  infcdaabs  8911  cfss  8970  tskuni  9484  ltexnq  9676  lt2addmuld  11159  div4p1lem1div2  11164  mul2lt0rgt0  11809  xrmax1  11880  xrmax2  11881  max1ALT  11891  qbtwnxr  11905  xleadd1a  11955  xlt2add  11962  xlesubadd  11965  xmulgt0  11985  xlemul1a  11990  xov1plusxeqvd  12189  uzsubsubfz  12234  fzctr  12320  subfzo0  12452  flflp1  12470  fldiv4lem1div2uz2  12499  ceilge  12507  modge0  12540  modlt  12541  modid  12557  m1modge3gt1  12579  modaddmodup  12595  sermono  12695  seqf1olem1  12702  seqf1olem2  12703  leexp1a  12781  sqgt0  12794  sqge0  12802  nnlesq  12830  expnbnd  12855  expmulnbnd  12858  discr1  12862  facwordi  12938  faclbnd5  12947  hashdom  13029  fi1uzind  13134  brfi1indALT  13137  fi1uzindOLD  13140  brfi1indALTOLD  13143  ccatws1n0  13261  swrds2  13533  cjmulge0  13734  resqrtcl  13842  absge0  13875  sqreulem  13947  amgm2  13957  rlimdm  14130  rlimge0  14160  reccn2  14175  climle  14218  climserle  14241  isercoll2  14247  iseraltlem1  14260  iseralt  14263  isumclim2  14331  isumclim3  14332  isumge0  14339  fsumless  14369  cvgcmp  14389  cvgcmpce  14391  abscvgcvg  14392  isumsup2  14417  isumltss  14419  climcndslem1  14420  climcnds  14422  supcvg  14427  harmonic  14430  expcnv  14435  explecnv  14436  cvgrat  14454  mertenslem1  14455  mertenslem2  14456  clim2div  14460  ntrivcvgtail  14471  iprodclim2  14569  iprodclim3  14570  efcvg  14654  ege2le3  14659  efaddlem  14662  eftlub  14678  effsumlt  14680  tanhlt1  14729  ef01bndlem  14753  sin02gt0  14761  rpnnen2lem4  14785  ruclem2  14800  ruclem3  14801  ruclem9  14806  iddvdsexp  14843  dvdsadd  14862  dvdsfac  14886  dvdsmod  14888  3dvds  14890  3dvdsOLD  14891  omoe  14926  sumeven  14948  divalglem1  14955  flodddiv4t2lthalf  14978  bitsfzo  14995  bitsmod  14996  bitscmp  14998  bitsinv1lem  15001  sadcaddlem  15017  sadadd3  15021  sadaddlem  15026  dvdssqim  15111  dvdsmulgcd  15112  nn0seqcvgd  15121  dvdslcm  15149  lcmgcdlem  15157  dvdslcmf  15182  lcmfunsnlem2lem2  15190  mulgcddvds  15207  qredeq  15209  cncongr2  15220  sqnprm  15252  isprm6  15264  nonsq  15305  hashdvds  15318  prmdiv  15328  odzdvds  15338  pythagtriplem4  15362  pcpre1  15385  pcdvdsb  15411  pcz  15423  pcprmpw2  15424  pcaddlem  15430  pcadd  15431  pcadd2  15432  pcmpt  15434  pcmptdvds  15436  fldivp1  15439  pcfaclem  15440  pockthlem  15447  prmreclem1  15458  prmreclem3  15460  prmreclem5  15462  prmreclem6  15463  4sqlem6  15485  4sqlem8  15487  4sqlem11  15497  4sqlem12  15498  4sqlem14  15500  4sqlem16  15502  vdwlem3  15525  vdwlem9  15531  vdwlem10  15532  vdwlem12  15534  ramub1lem2  15569  prmgap  15601  prmgaplcm  15602  prmgapprmo  15604  mreexexd  16131  invfuc  16457  ple1  16867  eqgen  17470  lagsubg  17479  pgpfi  17843  sylow2alem2  17856  sylow2a  17857  sylow3lem4  17868  efgsrel  17970  odadd1  18074  odadd2  18075  gexex  18079  lt6abl  18119  dprd2d2  18266  dmdprdpr  18271  ablfacrp2  18289  ablfac1c  18293  pgpfaclem1  18303  ablfac2  18311  dvdsrmul1  18476  unitmulclb  18488  subrguss  18618  abvres  18662  ply1coefsupp  19486  evl1gsumadd  19543  znfld  19728  znunit  19731  frlmisfrlm  20006  matgsum  20062  pm2mpcl  20421  psmetxrge0  21928  isxmet2d  21942  mettri  21967  xmettri3  21968  mettri3  21969  xmetrtri2  21971  prdsxmetlem  21983  imasdsf1olem  21988  xblss2ps  22016  blss2ps  22018  blss2  22019  blssps  22039  blss  22040  prdsbl  22106  dscmet  22187  nmge0  22231  nmmtri  22236  tngngp3  22270  nlmvscnlem2  22299  nrginvrcnlem  22305  nmoix  22343  nmoleub  22345  blcvx  22409  xrsxmet  22420  opnreen  22442  xrge0tsms  22445  icopnfcnv  22549  xrhmeo  22553  lebnumii  22573  pcophtb  22637  pi1grplem  22657  nmoleub2lem  22722  ipcau2  22841  tchcphlem1  22842  ipcau  22845  ipcnlem2  22851  rrxcph  22988  minveclem2  23005  minveclem3b  23007  pjthlem1  23016  pjthlem2  23017  ivthlem3  23029  ivth2  23031  ovolfsf  23047  ovolsslem  23059  ovollb2lem  23063  ovollb2  23064  ovolctb  23065  ovolfiniun  23076  ovolicc1  23091  ovolicc2lem4  23095  ovolicc2  23097  nulmbl2  23111  unmbl  23112  ioombl1lem4  23136  uniioombllem4  23160  uniioombllem6  23162  volivth  23181  vitalilem4  23186  itg1ge0  23259  itg1ge0a  23284  itg1lea  23285  itg1climres  23287  mbfi1fseqlem5  23292  itg2ub  23306  itg2seq  23315  itg2uba  23316  itg2splitlem  23321  itg2split  23322  itg2monolem3  23325  itg2mono  23326  itg2i1fseq2  23329  itg2addlem  23331  iblss  23377  itggt0  23414  dvferm2lem  23553  dvlip  23560  dvivthlem1  23575  dvfsumlem2  23594  dvfsumlem3  23595  ftc1lem4  23606  ply1divmo  23699  ply1remlem  23726  fta1glem2  23730  ig1pdvds  23740  plyeq0lem  23770  plydiveu  23857  fta1lem  23866  vieta1lem2  23870  aaliou3lem2  23902  aaliou3lem8  23904  ulmcn  23957  mtest  23962  itgulm  23966  radcnvlem1  23971  radcnvlt1  23976  dvradcnv  23979  pserdvlem2  23986  abelthlem2  23990  abelthlem6  23994  abelthlem7  23996  abelthlem9  23998  tangtx  24061  sinq12gt0  24063  sineq0  24077  cosordlem  24081  tanord  24088  tanregt0  24089  logrnaddcl  24125  logcj  24156  argregt0  24160  argrege0  24161  argimgt0  24162  argimlt0  24163  logimul  24164  logneg2  24165  logdivlti  24170  divlogrlim  24181  logcnlem3  24190  logcnlem4  24191  dvlog2lem  24198  logtayl  24206  rpcxpcl  24222  cxpsqrtlem  24248  cxpaddle  24293  isosctrlem1  24348  asinlem3a  24397  asinlem3  24398  asinneg  24413  asinsinlem  24418  asinsin  24419  atanlogaddlem  24440  atanlogadd  24441  atanlogsublem  24442  atanlogsub  24443  atantan  24450  atanbndlem  24452  atantayl  24464  leibpi  24469  birthdaylem3  24480  areaf  24488  cxploglim  24504  jensenlem2  24514  jensen  24515  logdiflbnd  24521  harmonicbnd4  24537  fsumharmonic  24538  zetacvg  24541  lgamgulmlem2  24556  lgamgulmlem3  24557  lgamcvg2  24581  wilthlem2  24595  wilthimp  24598  ftalem1  24599  ftalem2  24600  ftalem5  24603  basellem6  24612  basellem8  24614  basellem9  24615  chtge0  24638  chtublem  24736  logexprlim  24750  perfectlem1  24754  bcmax  24803  bposlem1  24809  bposlem2  24810  bposlem6  24814  bposlem7  24815  lgsdilem2  24858  lgsqrlem4  24874  lgsquadlem1  24905  2lgsoddprmlem2  24934  2sqlem3  24945  2sqlem8  24951  2sqblem  24956  chebbnd1lem2  24959  chtppilimlem1  24962  chtppilim  24964  chto1ub  24965  vmadivsum  24971  rplogsumlem1  24973  rplogsumlem2  24974  dchrisum0lem1a  24975  rpvmasumlem  24976  dchrisumlem1  24978  dchrisumlem2  24979  dchrvmasumlem2  24987  dchrisum0flblem1  24997  dchrisum0flblem2  24998  dchrisum0lem1b  25004  dchrisum0lem1  25005  dchrisum0lem2a  25006  dchrisum0lem3  25008  dchrisum0  25009  mudivsum  25019  mulogsumlem  25020  mulog2sumlem1  25023  mulog2sumlem2  25024  2vmadivsumlem  25029  chpdifbndlem1  25042  selberg3lem1  25046  selberg4lem1  25049  pntrlog2bndlem1  25066  pntrlog2bndlem2  25067  pntrlog2bndlem3  25068  pntrlog2bndlem4  25069  pntpbnd1a  25074  pntpbnd1  25075  pntpbnd2  25076  pntibndlem2  25080  pntibndlem3  25081  pntlemd  25083  pntlemc  25084  pntlemb  25086  pntlemg  25087  pntlemh  25088  pntlemr  25091  pntlemf  25094  pntlemo  25096  abvcxp  25104  ostth2lem1  25107  padicabv  25119  ostth2lem2  25123  ostth2lem3  25124  ostth2lem4  25125  ostth2  25126  ostth3  25127  tgcgr4  25226  legso  25294  krippenlem  25385  midex  25429  oppperpex  25445  ttgcontlem1  25565  axpaschlem  25620  axcontlem8  25651  upgrex  25759  umgraex  25852  wwlkextproplem3  26271  clwlkisclwwlk2  26318  clwwlkndivn  26364  clwlkf1clwwlklem1  26373  ex-ind-dvds  26710  nvabs  26911  nmooge0  27006  nmoolb  27010  siii  27092  minvecolem2  27115  minvecolem4  27120  minvecolem5  27121  hlipgt0  27154  normge0  27367  normpyc  27387  pjhthlem1  27634  pjige0i  27933  nmoplb  28150  nmfnlb  28167  branmfn  28348  pjssdif2i  28417  stlei  28483  xlt2addrd  28913  eliccelico  28929  elicoelioo  28930  bcm1n  28941  2sqmod  28979  omndmul2  29043  archirngz  29074  archiabllem2c  29080  xrge0tsmsd  29116  ofldchr  29145  psgnfzto1stlem  29181  madjusmdetlem2  29222  locfinreflem  29235  xrge0iifiso  29309  nexple  29399  gsumesum  29448  esumcst  29452  esumpcvgval  29467  esumcvg  29475  esumiun  29483  measssd  29605  measunl  29606  omssubadd  29689  carsgclctunlem3  29709  pmeasmono  29713  sibfof  29729  oddpwdc  29743  eulerpartlemgc  29751  iwrdsplit  29776  ballotlemsgt1  29899  ballotlemsel1i  29901  sgnmul  29931  signsply0  29954  signstfvc  29977  signsvtp  29986  signsvfpn  29988  subfaclim  30424  erdszelem7  30433  erdszelem8  30434  cvmliftlem2  30522  snmlff  30565  sinccvglem  30820  climlec3  30872  faclim  30885  dvdspw  30889  nodense  31088  nobndup  31099  fnejoin1  31533  poimirlem12  32591  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem23  32602  poimirlem28  32607  broucube  32613  mblfinlem2  32617  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  itg2addnclem  32631  itg2addnclem3  32633  itg2gt0cn  32635  itggt0cn  32652  ftc1anclem5  32659  ftc1anclem7  32661  ftc1anclem8  32662  isbnd3  32753  ssbnd  32757  heiborlem8  32787  bfplem2  32792  rrncmslem  32801  rrnequiv  32804  rrntotbnd  32805  lcv1  33346  lsatcv0eq  33352  lsatcvat3  33357  cvlsupr2  33648  hlatlej2  33680  cvrval4N  33718  cvratlem  33725  atcvr0eq  33730  2atlt  33743  atbtwnex  33752  athgt  33760  1cvrat  33780  ps-1  33781  hlatexch3N  33784  hlatexch4  33785  3atlem2  33788  atcvrlln2  33823  lplnexllnN  33868  4atlem3a  33901  4atlem10b  33909  4atlem11b  33912  4atlem12b  33915  2lplnja  33923  dalemply  33958  dalemsly  33959  dalem1  33963  dalem6  33972  dalem7  33973  dalem-cly  33975  dalem11  33978  dalem12  33979  dalem16  33983  dalem17  33984  dalem38  34014  dalem44  34020  dalem61  34037  lnatexN  34083  lncvrat  34086  lncmp  34087  paddasslem2  34125  dalawlem3  34177  dalawlem6  34180  dalawlem11  34185  lhpmcvr  34327  lhp2atne  34338  lhp2at0ne  34340  lautj  34397  trlval4  34493  cdlemc2  34497  cdlemc5  34500  cdleme3b  34534  cdleme11c  34566  cdleme19a  34609  cdleme20j  34624  cdleme22f  34652  cdleme23c  34657  cdleme26f2ALTN  34670  cdleme26f2  34671  cdleme35fnpq  34755  cdleme48bw  34808  cdlemg10a  34946  cdlemg11b  34948  cdlemg17g  34973  cdlemg18c  34986  cdlemi1  35124  cdlemk52  35260  dia2dimlem1  35371  dihord1  35525  dihjatcclem4  35728  eldioph2lem1  36341  lzenom  36351  irrapxlem1  36404  irrapxlem4  36407  irrapxlem5  36408  pell14qrgt0  36441  pell1qrge1  36452  pell1qrgap  36456  pellfundge  36464  pellfundex  36468  pellfund14  36480  rmspecsqrtnq  36488  rmspecsqrtnqOLD  36489  rmxypos  36532  ltrmynn0  36533  ltrmxnn0  36534  jm2.24nn  36544  jm2.17b  36546  jm2.17c  36547  jm2.24  36548  congadd  36551  congsym  36553  congneg  36554  congid  36556  mzpcong  36557  acongrep  36565  acongeq  36568  jm2.18  36573  jm2.19  36578  jm2.23  36581  jm2.25  36584  jm2.26lem3  36586  jm2.15nn0  36588  jm2.16nn0  36589  jm2.27a  36590  jm2.27c  36592  jm3.1lem1  36602  idomrootle  36792  idomsubgmo  36795  inductionexd  37473  imo72b2  37497  dvgrat  37533  radcnvrat  37535  binomcxplemnn0  37570  binomcxplemnotnn0  37577  cncmpmax  38214  zltlesub  38438  fmul01  38647  fmul01lt1lem1  38651  climdivf  38679  sumnnodd  38697  dvdivbd  38813  volge0  38853  stoweidlem1  38894  stoweidlem16  38909  stoweidlem18  38911  stoweidlem24  38917  stoweidlem26  38919  stoweidlem36  38929  stoweidlem38  38931  stoweidlem41  38934  stoweidlem42  38935  stoweidlem44  38937  stoweidlem45  38938  stoweidlem48  38941  stoweidlem62  38955  wallispilem5  38962  stirlinglem1  38967  stirlinglem5  38971  stirlinglem7  38973  stirlinglem8  38974  stirlinglem9  38975  stirlinglem11  38977  fourierdlem4  39004  fourierdlem10  39010  fourierdlem37  39037  fourierdlem47  39046  fourierdlem72  39071  fourierdlem74  39073  fourierdlem79  39078  fourierdlem82  39081  fourierdlem89  39088  fourierdlem91  39090  fourierdlem93  39092  fourierdlem103  39102  fourierdlem104  39103  fourierdlem112  39111  etransclem24  39151  etransclem25  39152  etransclem28  39155  etransclem37  39164  etransclem38  39165  etransclem44  39171  vonicclem1  39574  pimconstlt0  39591  rlimdmafv  39906  iccpartgtprec  39958  iccpartlt  39962  iccpartgtl  39964  sqrtpwpw2p  39988  fmtnodvds  39994  goldbachthlem1  39995  lighneallem4a  40063  perfectALTVlem1  40164  2elfz2melfz  40355  nfile  40369  nbfusgrlevtxm1  40605  wwlksnextproplem3  41117  clwlkclwwlk2  41212  clwwlksndivn  41264  clwlksf1clwwlklem1  41272  av-extwwlkfablem2  41510  cznnring  41748  rhmsubcrngc  41821  altgsumbcALT  41924  expnegico01  42102  flnn0div2ge  42121  rege1logbrege0  42150  fllogbd  42152  fllog2  42160  nnpw2blen  42172  nnolog2flm1  42182  dignn0ldlem  42194  dignn0flhalflem1  42207  dignn0flhalflem2  42208
  Copyright terms: Public domain W3C validator