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

Theorem breqtrrd 4605
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 2615 . 2 (𝜑𝐵 = 𝐶)
41, 3breqtrd 4603 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:  marypha1lem  8199  marypha2  8205  unxpwdom  8354  uncdadom  8853  cdacomen  8863  cdaassen  8864  xpcdaen  8865  onacda  8879  infcdaabs  8888  cfss  8947  tskuni  9461  ltexnq  9653  lt2addmuld  11129  div4p1lem1div2  11134  mul2lt0rgt0  11765  xrmax1  11839  xrmax2  11840  max1ALT  11850  qbtwnxr  11864  xleadd1a  11912  xlt2add  11919  xlesubadd  11922  xmulgt0  11942  xlemul1a  11947  xov1plusxeqvd  12145  uzsubsubfz  12189  fzctr  12275  subfzo0  12407  flflp1  12425  fldiv4lem1div2uz2  12454  ceilge  12462  modge0  12495  modlt  12496  modid  12512  m1modge3gt1  12534  modaddmodup  12550  sermono  12650  seqf1olem1  12657  seqf1olem2  12658  leexp1a  12736  sqgt0  12749  sqge0  12757  nnlesq  12785  expnbnd  12810  expmulnbnd  12813  discr1  12817  facwordi  12893  faclbnd5  12902  hashdom  12981  fi1uzind  13080  brfi1indALT  13083  fi1uzindOLD  13086  brfi1indALTOLD  13089  ccatws1n0  13207  swrds2  13479  cjmulge0  13680  resqrtcl  13788  absge0  13821  sqreulem  13893  amgm2  13903  rlimdm  14076  rlimge0  14106  reccn2  14121  climle  14164  climserle  14187  isercoll2  14193  iseraltlem1  14206  iseralt  14209  isumclim2  14277  isumclim3  14278  isumge0  14285  fsumless  14315  cvgcmp  14335  cvgcmpce  14337  abscvgcvg  14338  isumsup2  14363  isumltss  14365  climcndslem1  14366  climcnds  14368  supcvg  14373  harmonic  14376  expcnv  14381  explecnv  14382  cvgrat  14400  mertenslem1  14401  mertenslem2  14402  clim2div  14406  ntrivcvgtail  14417  iprodclim2  14515  iprodclim3  14516  efcvg  14600  ege2le3  14605  efaddlem  14608  eftlub  14624  effsumlt  14626  tanhlt1  14675  ef01bndlem  14699  sin02gt0  14707  rpnnen2lem4  14731  ruclem2  14746  ruclem3  14747  ruclem9  14752  iddvdsexp  14789  dvdsadd  14808  dvdsfac  14832  dvdsmod  14834  3dvds  14836  3dvdsOLD  14837  omoe  14872  sumeven  14894  divalglem1  14901  flodddiv4t2lthalf  14924  bitsfzo  14941  bitsmod  14942  bitscmp  14944  bitsinv1lem  14947  sadcaddlem  14963  sadadd3  14967  sadaddlem  14972  dvdssqim  15057  dvdsmulgcd  15058  nn0seqcvgd  15067  dvdslcm  15095  lcmgcdlem  15103  dvdslcmf  15128  lcmfunsnlem2lem2  15136  mulgcddvds  15153  qredeq  15155  cncongr2  15166  sqnprm  15198  isprm6  15210  nonsq  15251  hashdvds  15264  prmdiv  15274  odzdvds  15284  pythagtriplem4  15308  pcpre1  15331  pcdvdsb  15357  pcz  15369  pcprmpw2  15370  pcaddlem  15376  pcadd  15377  pcadd2  15378  pcmpt  15380  pcmptdvds  15382  fldivp1  15385  pcfaclem  15386  pockthlem  15393  prmreclem1  15404  prmreclem3  15406  prmreclem5  15408  prmreclem6  15409  4sqlem6  15431  4sqlem8  15433  4sqlem11  15443  4sqlem12  15444  4sqlem14  15446  4sqlem16  15448  vdwlem3  15471  vdwlem9  15477  vdwlem10  15478  vdwlem12  15480  ramub1lem2  15515  prmgap  15547  prmgaplcm  15548  prmgapprmo  15550  mreexexd  16077  invfuc  16403  ple1  16813  eqgen  17416  lagsubg  17425  pgpfi  17789  sylow2alem2  17802  sylow2a  17803  sylow3lem4  17814  efgsrel  17916  odadd1  18020  odadd2  18021  gexex  18025  lt6abl  18065  dprd2d2  18212  dmdprdpr  18217  ablfacrp2  18235  ablfac1c  18239  pgpfaclem1  18249  ablfac2  18257  dvdsrmul1  18422  unitmulclb  18434  subrguss  18564  abvres  18608  ply1coefsupp  19432  evl1gsumadd  19489  znfld  19673  znunit  19676  frlmisfrlm  19948  matgsum  20004  pm2mpcl  20363  psmetxrge0  21870  isxmet2d  21883  mettri  21908  xmettri3  21909  mettri3  21910  xmetrtri2  21912  prdsxmetlem  21924  imasdsf1olem  21929  xblss2ps  21957  blss2ps  21959  blss2  21960  blssps  21980  blss  21981  prdsbl  22047  dscmet  22128  nmge0  22171  nmmtri  22176  nlmvscnlem2  22232  nrginvrcnlem  22238  nmoix  22275  nmoleub  22277  blcvx  22341  xrsxmet  22352  opnreen  22374  xrge0tsms  22377  icopnfcnv  22480  xrhmeo  22484  lebnumii  22504  pcophtb  22568  pi1grplem  22588  nmoleub2lem  22653  ipcau2  22762  tchcphlem1  22763  ipcau  22766  ipcnlem2  22769  rrxcph  22905  minveclem2  22922  minveclem3b  22924  pjthlem1  22933  pjthlem2  22934  ivthlem3  22946  ivth2  22948  ovolfsf  22964  ovolsslem  22976  ovollb2lem  22980  ovollb2  22981  ovolctb  22982  ovolfiniun  22993  ovolicc1  23008  ovolicc2lem4  23012  ovolicc2  23014  nulmbl2  23028  unmbl  23029  ioombl1lem4  23053  uniioombllem4  23077  uniioombllem6  23079  volivth  23098  vitalilem4  23103  itg1ge0  23176  itg1ge0a  23201  itg1lea  23202  itg1climres  23204  mbfi1fseqlem5  23209  itg2ub  23223  itg2seq  23232  itg2uba  23233  itg2splitlem  23238  itg2split  23239  itg2monolem3  23242  itg2mono  23243  itg2i1fseq2  23246  itg2addlem  23248  iblss  23294  itggt0  23331  dvferm2lem  23470  dvlip  23477  dvivthlem1  23492  dvfsumlem2  23511  dvfsumlem3  23512  ftc1lem4  23523  ply1divmo  23616  ply1remlem  23643  fta1glem2  23647  ig1pdvds  23657  plyeq0lem  23687  plydiveu  23774  fta1lem  23783  vieta1lem2  23787  aaliou3lem2  23819  aaliou3lem8  23821  ulmcn  23874  mtest  23879  itgulm  23883  radcnvlem1  23888  radcnvlt1  23893  dvradcnv  23896  pserdvlem2  23903  abelthlem2  23907  abelthlem6  23911  abelthlem7  23913  abelthlem9  23915  tangtx  23978  sinq12gt0  23980  sineq0  23994  cosordlem  23998  tanord  24005  tanregt0  24006  logrnaddcl  24042  logcj  24073  argregt0  24077  argrege0  24078  argimgt0  24079  argimlt0  24080  logimul  24081  logneg2  24082  logdivlti  24087  divlogrlim  24098  logcnlem3  24107  logcnlem4  24108  dvlog2lem  24115  logtayl  24123  rpcxpcl  24139  cxpsqrtlem  24165  cxpaddle  24210  isosctrlem1  24265  asinlem3a  24314  asinlem3  24315  asinneg  24330  asinsinlem  24335  asinsin  24336  atanlogaddlem  24357  atanlogadd  24358  atanlogsublem  24359  atanlogsub  24360  atantan  24367  atanbndlem  24369  atantayl  24381  leibpi  24386  birthdaylem3  24397  areaf  24405  cxploglim  24421  jensenlem2  24431  jensen  24432  logdiflbnd  24438  harmonicbnd4  24454  fsumharmonic  24455  zetacvg  24458  lgamgulmlem2  24473  lgamgulmlem3  24474  lgamcvg2  24498  wilthlem2  24512  wilthimp  24515  ftalem1  24516  ftalem2  24517  ftalem5  24520  basellem6  24529  basellem8  24531  basellem9  24532  chtge0  24555  chtublem  24653  logexprlim  24667  perfectlem1  24671  bcmax  24720  bposlem1  24726  bposlem2  24727  bposlem6  24731  bposlem7  24732  lgsdilem2  24775  lgsqrlem4  24791  lgsquadlem1  24822  2lgsoddprmlem2  24851  2sqlem3  24862  2sqlem8  24868  2sqblem  24873  chebbnd1lem2  24876  chtppilimlem1  24879  chtppilim  24881  chto1ub  24882  vmadivsum  24888  rplogsumlem1  24890  rplogsumlem2  24891  dchrisum0lem1a  24892  rpvmasumlem  24893  dchrisumlem1  24895  dchrisumlem2  24896  dchrvmasumlem2  24904  dchrisum0flblem1  24914  dchrisum0flblem2  24915  dchrisum0lem1b  24921  dchrisum0lem1  24922  dchrisum0lem2a  24923  dchrisum0lem3  24925  dchrisum0  24926  mudivsum  24936  mulogsumlem  24937  mulog2sumlem1  24940  mulog2sumlem2  24941  2vmadivsumlem  24946  chpdifbndlem1  24959  selberg3lem1  24963  selberg4lem1  24966  pntrlog2bndlem1  24983  pntrlog2bndlem2  24984  pntrlog2bndlem3  24985  pntrlog2bndlem4  24986  pntpbnd1a  24991  pntpbnd1  24992  pntpbnd2  24993  pntibndlem2  24997  pntibndlem3  24998  pntlemd  25000  pntlemc  25001  pntlemb  25003  pntlemg  25004  pntlemh  25005  pntlemr  25008  pntlemf  25011  pntlemo  25013  abvcxp  25021  ostth2lem1  25024  padicabv  25036  ostth2lem2  25040  ostth2lem3  25041  ostth2lem4  25042  ostth2  25043  ostth3  25044  tgcgr4  25144  legso  25212  krippenlem  25303  midex  25347  oppperpex  25363  ttgcontlem1  25483  axpaschlem  25538  axcontlem8  25569  umgraex  25618  wwlkextproplem3  26037  clwlkisclwwlk2  26084  clwwlkndivn  26130  clwlkf1clwwlklem1  26139  ex-ind-dvds  26476  nvabs  26706  nmooge0  26812  nmoolb  26816  siii  26898  minvecolem2  26921  minvecolem4  26926  minvecolem5  26927  hlipgt0  26960  normge0  27173  normpyc  27193  pjhthlem1  27440  pjige0i  27739  nmoplb  27956  nmfnlb  27973  branmfn  28154  pjssdif2i  28223  stlei  28289  xlt2addrd  28719  eliccelico  28735  elicoelioo  28736  bcm1n  28747  2sqmod  28785  omndmul2  28849  archirngz  28880  archiabllem2c  28886  xrge0tsmsd  28922  ofldchr  28951  psgnfzto1stlem  28987  madjusmdetlem2  29028  locfinreflem  29041  xrge0iifiso  29115  nexple  29205  gsumesum  29254  esumcst  29258  esumpcvgval  29273  esumcvg  29281  esumiun  29289  measssd  29411  measunl  29412  omssubadd  29495  carsgclctunlem3  29515  pmeasmono  29519  sibfof  29535  oddpwdc  29549  eulerpartlemgc  29557  iwrdsplit  29582  ballotlemsgt1  29705  ballotlemsel1i  29707  sgnmul  29737  signsply0  29760  signstfvc  29783  signsvtp  29792  signsvfpn  29794  subfaclim  30230  erdszelem7  30239  erdszelem8  30240  cvmliftlem2  30328  snmlff  30371  sinccvglem  30626  climlec3  30678  faclim  30691  dvdspw  30695  nodense  30894  nobndup  30905  fnejoin1  31339  poimirlem12  32387  poimirlem17  32392  poimirlem19  32394  poimirlem20  32395  poimirlem23  32398  poimirlem28  32403  broucube  32409  mblfinlem2  32413  mblfinlem3  32414  mblfinlem4  32415  ismblfin  32416  itg2addnclem  32427  itg2addnclem3  32429  itg2gt0cn  32431  itggt0cn  32448  ftc1anclem5  32455  ftc1anclem7  32457  ftc1anclem8  32458  isbnd3  32549  ssbnd  32553  heiborlem8  32583  bfplem2  32588  rrncmslem  32597  rrnequiv  32600  rrntotbnd  32601  lcv1  33142  lsatcv0eq  33148  lsatcvat3  33153  cvlsupr2  33444  hlatlej2  33476  cvrval4N  33514  cvratlem  33521  atcvr0eq  33526  2atlt  33539  atbtwnex  33548  athgt  33556  1cvrat  33576  ps-1  33577  hlatexch3N  33580  hlatexch4  33581  3atlem2  33584  atcvrlln2  33619  lplnexllnN  33664  4atlem3a  33697  4atlem10b  33705  4atlem11b  33708  4atlem12b  33711  2lplnja  33719  dalemply  33754  dalemsly  33755  dalem1  33759  dalem6  33768  dalem7  33769  dalem-cly  33771  dalem11  33774  dalem12  33775  dalem16  33779  dalem17  33780  dalem38  33810  dalem44  33816  dalem61  33833  lnatexN  33879  lncvrat  33882  lncmp  33883  paddasslem2  33921  dalawlem3  33973  dalawlem6  33976  dalawlem11  33981  lhpmcvr  34123  lhp2atne  34134  lhp2at0ne  34136  lautj  34193  trlval4  34289  cdlemc2  34293  cdlemc5  34296  cdleme3b  34330  cdleme11c  34362  cdleme19a  34405  cdleme20j  34420  cdleme22f  34448  cdleme23c  34453  cdleme26f2ALTN  34466  cdleme26f2  34467  cdleme35fnpq  34551  cdleme48bw  34604  cdlemg10a  34742  cdlemg11b  34744  cdlemg17g  34769  cdlemg18c  34782  cdlemi1  34920  cdlemk52  35056  dia2dimlem1  35167  dihord1  35321  dihjatcclem4  35524  eldioph2lem1  36137  lzenom  36147  irrapxlem1  36200  irrapxlem4  36203  irrapxlem5  36204  pell14qrgt0  36237  pell1qrge1  36248  pell1qrgap  36252  pellfundge  36260  pellfundex  36264  pellfund14  36276  rmspecsqrtnq  36284  rmspecsqrtnqOLD  36285  rmxypos  36328  ltrmynn0  36329  ltrmxnn0  36330  jm2.24nn  36340  jm2.17b  36342  jm2.17c  36343  jm2.24  36344  congadd  36347  congsym  36349  congneg  36350  congid  36352  mzpcong  36353  acongrep  36361  acongeq  36364  jm2.18  36369  jm2.19  36374  jm2.23  36377  jm2.25  36380  jm2.26lem3  36382  jm2.15nn0  36384  jm2.16nn0  36385  jm2.27a  36386  jm2.27c  36388  jm3.1lem1  36398  idomrootle  36588  idomsubgmo  36591  inductionexd  37269  imo72b2  37293  dvgrat  37329  radcnvrat  37331  binomcxplemnn0  37366  binomcxplemnotnn0  37373  cncmpmax  38010  zltlesub  38234  fmul01  38444  fmul01lt1lem1  38448  climdivf  38476  sumnnodd  38494  dvdivbd  38610  volge0  38650  stoweidlem1  38691  stoweidlem16  38706  stoweidlem18  38708  stoweidlem24  38714  stoweidlem26  38716  stoweidlem36  38726  stoweidlem38  38728  stoweidlem41  38731  stoweidlem42  38732  stoweidlem44  38734  stoweidlem45  38735  stoweidlem48  38738  stoweidlem62  38752  wallispilem5  38759  stirlinglem1  38764  stirlinglem5  38768  stirlinglem7  38770  stirlinglem8  38771  stirlinglem9  38772  stirlinglem11  38774  fourierdlem4  38801  fourierdlem10  38807  fourierdlem37  38834  fourierdlem47  38843  fourierdlem72  38868  fourierdlem74  38870  fourierdlem79  38875  fourierdlem82  38878  fourierdlem89  38885  fourierdlem91  38887  fourierdlem93  38889  fourierdlem103  38899  fourierdlem104  38900  fourierdlem112  38908  etransclem24  38948  etransclem25  38949  etransclem28  38952  etransclem37  38961  etransclem38  38962  etransclem44  38968  vonicclem1  39371  pimconstlt0  39388  rlimdmafv  39704  iccpartgtprec  39756  iccpartlt  39760  iccpartgtl  39762  sqrtpwpw2p  39786  fmtnodvds  39792  goldbachthlem1  39793  lighneallem4a  39861  perfectALTVlem1  39962  2elfz2melfz  40175  nfile  40189  upgrex  40313  nbfusgrlevtxm1  40600  wwlksnextproplem3  41112  clwlkclwwlk2  41207  clwwlksndivn  41259  clwlksf1clwwlklem1  41267  av-extwwlkfablem2  41505  cznnring  41743  rhmsubcrngc  41816  altgsumbcALT  41919  expnegico01  42097  flnn0div2ge  42116  rege1logbrege0  42145  fllogbd  42147  fllog2  42155  nnpw2blen  42167  nnolog2flm1  42177  dignn0ldlem  42189  dignn0flhalflem1  42202  dignn0flhalflem2  42203
  Copyright terms: Public domain W3C validator