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

Theorem breqtrrd 4151
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
Hypotheses
Ref Expression
breqtrrd.1  |-  ( ph  ->  A R B )
breqtrrd.2  |-  ( ph  ->  C  =  B )
Assertion
Ref Expression
breqtrrd  |-  ( ph  ->  A R C )

Proof of Theorem breqtrrd
StepHypRef Expression
1 breqtrrd.1 . 2  |-  ( ph  ->  A R B )
2 breqtrrd.2 . . 3  |-  ( ph  ->  C  =  B )
32eqcomd 2371 . 2  |-  ( ph  ->  B  =  C )
41, 3breqtrd 4149 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1647   class class class wbr 4125
This theorem is referenced by:  marypha1lem  7333  marypha2  7339  unxpwdom  7450  uncdadom  7944  cdacomen  7954  cdaassen  7955  xpcdaen  7956  onacda  7970  infcdaabs  7979  cfss  8038  tskuni  8552  ltexnq  8746  xrmax1  10656  xrmax2  10657  max1ALT  10667  qbtwnxr  10679  xleadd1a  10725  xlt2add  10732  xlesubadd  10735  xmulgt0  10755  xlemul1a  10760  xov1plusxeqvd  10933  fzctr  11007  modge0  11144  modlt  11145  modid  11157  sermono  11242  seqf1olem1  11249  seqf1olem2  11250  leexp1a  11325  sqgt0  11337  sqge0  11345  nnlesq  11371  expnbnd  11395  expmulnbnd  11398  discr1  11402  facwordi  11467  faclbnd5  11476  hashdom  11540  hashge1  11550  brfi1uzind  11602  swrds2  11767  cjmulge0  11838  resqrcl  11946  absge0  11979  sqreulem  12050  amgm2  12060  rlimdm  12232  rlimge0  12262  reccn2  12277  climle  12320  climserle  12343  isercoll2  12349  iseraltlem1  12362  iseralt  12365  isumclim2  12429  isumclim3  12430  isumge0  12437  fsumless  12462  cvgcmp  12482  cvgcmpce  12484  abscvgcvg  12485  isumsup2  12513  isumltss  12515  climcndslem1  12516  climcnds  12518  supcvg  12522  harmonic  12525  expcnv  12530  explecnv  12531  cvgrat  12547  mertenslem1  12548  mertenslem2  12549  efcvg  12574  ege2le3  12579  efaddlem  12582  eftlub  12597  effsumlt  12599  tanhlt1  12648  ef01bndlem  12672  sin02gt0  12680  rpnnen2lem4  12704  ruclem2  12718  ruclem3  12719  ruclem9  12724  iddvdsexp  12760  dvdsadd  12775  dvdsfac  12791  dvdsmod  12793  3dvds  12799  divalglem1  12801  bitsfzo  12834  bitsmod  12835  bitscmp  12837  bitsinv1lem  12840  sadcaddlem  12856  sadadd3  12860  sadaddlem  12865  dvdssqim  12940  dvdsmulgcd  12941  nn0seqcvgd  12948  sqnprm  12985  mulgcddvds  12991  qredeq  12993  isprm6  12996  nonsq  13038  hashdvds  13051  prmdiv  13061  odzdvds  13068  omoe  13073  pythagtriplem4  13080  pcpre1  13103  pcdvdsb  13129  pcz  13141  pcprmpw2  13142  pcaddlem  13144  pcadd  13145  pcadd2  13146  pcmpt  13148  pcmptdvds  13150  fldivp1  13153  pcfaclem  13154  pockthlem  13160  prmreclem1  13171  prmreclem3  13173  prmreclem5  13175  prmreclem6  13176  4sqlem6  13198  4sqlem8  13200  4sqlem11  13210  4sqlem12  13211  4sqlem14  13213  4sqlem16  13215  vdwlem3  13238  vdwlem9  13244  vdwlem10  13245  vdwlem12  13247  ramub1lem2  13282  invfuc  14058  ple1  14360  eqgen  14880  lagsubg  14889  pgpfi  15126  sylow2alem2  15139  sylow2a  15140  sylow3lem4  15151  efgsrel  15253  odadd1  15350  odadd2  15351  gexex  15355  lt6abl  15391  dprd2d2  15489  dmdprdpr  15494  ablfacrp2  15512  ablfac1c  15516  pgpfaclem1  15526  ablfac2  15534  dvdsrmul1  15645  unitmulclb  15657  subrguss  15770  abvres  15814  znfld  16731  znunit  16734  isxmet2d  18105  mettri  18129  xmettri3  18130  mettri3  18131  xmetrtri2  18133  prdsxmetlem  18145  imasdsf1olem  18150  blss2  18172  blss  18185  prdsbl  18250  dscmet  18308  nmge0  18351  nmmtri  18356  nlmvscnlem2  18409  nrginvrcnlem  18414  nmoix  18451  nmoleub  18453  blcvx  18517  xrsxmet  18528  opnreen  18550  xrge0tsms  18553  icopnfcnv  18655  xrhmeo  18659  lebnumii  18679  pcophtb  18742  pi1grplem  18762  nmoleub2lem  18810  ipcau2  18879  tchcphlem1  18880  ipcau  18883  ipcnlem2  18886  minveclem2  19005  minveclem3b  19007  pjthlem1  19016  pjthlem2  19017  ivthlem3  19028  ivth2  19030  ovolfsf  19046  ovolsslem  19058  ovollb2lem  19062  ovollb2  19063  ovolctb  19064  ovolfiniun  19075  ovolicc1  19090  ovolicc2lem4  19094  ovolicc2  19096  nulmbl2  19109  unmbl  19110  ioombl1lem4  19133  uniioombllem4  19156  uniioombllem6  19158  volivth  19177  vitalilem4  19181  itg1ge0  19256  itg1ge0a  19281  itg1lea  19282  itg1climres  19284  mbfi1fseqlem5  19289  itg2ub  19303  itg2seq  19312  itg2uba  19313  itg2splitlem  19318  itg2split  19319  itg2monolem3  19322  itg2mono  19323  itg2i1fseq2  19326  itg2addlem  19328  iblss  19374  itggt0  19411  dvferm2lem  19548  dvlip  19555  dvivthlem1  19570  dvfsumlem2  19589  dvfsumlem3  19590  ftc1lem4  19601  ply1divmo  19736  ply1remlem  19763  fta1glem2  19767  ig1pdvds  19777  plyeq0lem  19807  plydiveu  19893  fta1lem  19902  vieta1lem2  19906  aaliou3lem2  19938  aaliou3lem8  19940  ulmcn  19993  mtest  19998  itgulm  20002  radcnvlem1  20007  radcnvlt1  20012  dvradcnv  20015  pserdvlem2  20022  abelthlem2  20026  abelthlem6  20030  abelthlem7  20032  abelthlem9  20034  tangtx  20091  sinq12gt0  20093  sineq0  20107  cosordlem  20111  tanord  20118  tanregt0  20119  logrnaddcl  20150  logcj  20179  argregt0  20183  argrege0  20184  argimgt0  20185  argimlt0  20186  logimul  20187  logneg2  20188  logdivlti  20193  divlogrlim  20204  logcnlem3  20213  logcnlem4  20214  dvlog2lem  20221  logtayl  20229  rpcxpcl  20245  cxpsqrlem  20271  cxpaddle  20314  isosctrlem1  20340  asinlem3a  20388  asinlem3  20389  asinneg  20404  asinsinlem  20409  asinsin  20410  atanlogaddlem  20431  atanlogadd  20432  atanlogsublem  20433  atanlogsub  20434  atantan  20441  atanbndlem  20443  atantayl  20455  leibpi  20460  birthdaylem3  20470  areaf  20478  cxploglim  20494  jensenlem2  20504  jensen  20505  logdiflbnd  20511  harmonicbnd4  20527  fsumharmonic  20528  wilthlem2  20530  ftalem1  20533  ftalem2  20534  ftalem5  20537  basellem6  20546  basellem8  20548  basellem9  20549  chtge0  20573  chtublem  20673  logexprlim  20687  perfectlem1  20691  bcmax  20740  bposlem1  20746  bposlem2  20747  bposlem6  20751  bposlem7  20752  lgsdilem2  20793  lgsqrlem4  20806  lgsquadlem1  20816  2sqlem3  20828  2sqlem8  20834  2sqblem  20839  chebbnd1lem2  20842  chtppilimlem1  20845  chtppilim  20847  chto1ub  20848  vmadivsum  20854  rplogsumlem1  20856  rplogsumlem2  20857  dchrisum0lem1a  20858  rpvmasumlem  20859  dchrisumlem1  20861  dchrisumlem2  20862  dchrvmasumlem2  20870  dchrisum0flblem1  20880  dchrisum0flblem2  20881  dchrisum0lem1b  20887  dchrisum0lem1  20888  dchrisum0lem2a  20889  dchrisum0lem3  20891  dchrisum0  20892  mudivsum  20902  mulogsumlem  20903  mulog2sumlem1  20906  mulog2sumlem2  20907  2vmadivsumlem  20912  chpdifbndlem1  20925  selberg3lem1  20929  selberg4lem1  20932  pntrlog2bndlem1  20949  pntrlog2bndlem2  20950  pntrlog2bndlem3  20951  pntrlog2bndlem4  20952  pntpbnd1a  20957  pntpbnd1  20958  pntpbnd2  20959  pntibndlem2  20963  pntibndlem3  20964  pntlemd  20966  pntlemc  20967  pntlemb  20969  pntlemg  20970  pntlemh  20971  pntlemr  20974  pntlemf  20977  pntlemo  20979  abvcxp  20987  ostth2lem1  20990  padicabv  21002  ostth2lem2  21006  ostth2lem3  21007  ostth2lem4  21008  ostth2  21009  ostth3  21010  umgraex  21036  nvabs  21552  nmooge0  21658  nmoolb  21662  siii  21744  minvecolem2  21767  minvecolem4  21772  minvecolem5  21773  hlipgt0  21806  normge0  22018  normpyc  22038  pjhthlem1  22283  pjige0i  22582  nmoplb  22800  nmfnlb  22817  branmfn  22998  pjssdif2i  23067  stlei  23133  eliccelico  23541  elicoelioo  23542  xrge0tsmsd  23614  gsumesum  23916  esumcst  23920  esumpcvgval  23933  esumcvg  23941  measunl  24033  ballotlem5  24205  ballotlemsgt1  24216  ballotlemsel1i  24218  zetacvg  24247  lgamgulmlem2  24262  lgamgulmlem3  24263  lgamcvg2  24287  subfaclim  24322  erdszelem7  24331  erdszelem8  24332  cvmliftlem2  24420  snmlff  24499  sinccvglem  24592  climlec3  24698  clim2div  24701  ntrivcvgtail  24712  iprodclim2  24789  iprodclim3  24790  faclim  24840  dvdspw  24844  nodense  25084  nobndup  25095  axpaschlem  25310  axcontlem8  25341  lxflflp1  25670  itg2addnclem  25675  itg2addnc  25677  itg2gt0cn  25678  itggt0cn  25695  fnejoin1  25824  isbnd3  26014  ssbnd  26018  heiborlem8  26048  bfplem2  26053  rrncmslem  26062  rrnequiv  26065  rrntotbnd  26066  eldioph2lem1  26345  lzenom  26355  irrapxlem1  26413  irrapxlem4  26416  irrapxlem5  26417  pell14qrgt0  26450  pell1qrge1  26461  pell1qrgap  26465  pellfundge  26473  pellfundex  26477  pellfund14  26489  rmspecsqrnq  26497  rmxypos  26540  ltrmynn0  26541  ltrmxnn0  26542  jm2.24nn  26552  jm2.17b  26554  jm2.17c  26555  jm2.24  26556  congadd  26559  congsym  26561  congneg  26562  congid  26564  mzpcong  26565  acongrep  26573  acongeq  26576  jm2.18  26587  jm2.19  26592  jm2.23  26595  jm2.25  26598  jm2.26lem3  26600  jm2.15nn0  26602  jm2.16nn0  26603  jm2.27a  26604  jm2.27c  26606  jm3.1lem1  26616  idomrootle  27017  idomsubgmo  27020  cncmpmax  27209  fmul01  27216  fmul01lt1lem1  27220  climdivf  27244  stoweidlem1  27256  stoweidlem3  27258  stoweidlem16  27271  stoweidlem18  27273  stoweidlem26  27281  stoweidlem36  27291  stoweidlem38  27293  stoweidlem41  27296  stoweidlem42  27297  stoweidlem44  27299  stoweidlem45  27300  stoweidlem48  27303  stoweidlem51  27306  stoweidlem62  27317  wallispilem5  27324  stirlinglem1  27329  stirlinglem8  27336  stirlinglem9  27337  rlimdmafv  27548  lcv1  29302  lsatcv0eq  29308  lsatcvat3  29313  cvlsupr2  29604  hlatlej2  29636  cvrval4N  29674  cvratlem  29681  atcvr0eq  29686  2atlt  29699  atbtwnex  29708  athgt  29716  1cvrat  29736  ps-1  29737  hlatexch3N  29740  hlatexch4  29741  3atlem2  29744  atcvrlln2  29779  lplnexllnN  29824  4atlem3a  29857  4atlem10b  29865  4atlem11b  29868  4atlem12b  29871  2lplnja  29879  dalemply  29914  dalemsly  29915  dalem1  29919  dalem6  29928  dalem7  29929  dalem-cly  29931  dalem11  29934  dalem12  29935  dalem16  29939  dalem17  29940  dalem38  29970  dalem44  29976  dalem61  29993  lnatexN  30039  lncvrat  30042  lncmp  30043  paddasslem2  30081  dalawlem3  30133  dalawlem6  30136  dalawlem11  30141  lhpmcvr  30283  lhp2atne  30294  lhp2at0ne  30296  lautj  30353  trlval4  30448  cdlemc2  30452  cdlemc5  30455  cdleme3b  30489  cdleme11c  30521  cdleme19a  30563  cdleme20j  30578  cdleme22f  30606  cdleme23c  30611  cdleme26f2ALTN  30624  cdleme26f2  30625  cdleme35fnpq  30709  cdleme48bw  30762  cdlemg10a  30900  cdlemg11b  30902  cdlemg17g  30927  cdlemg18c  30940  cdlemi1  31078  cdlemk52  31214  dia2dimlem1  31325  dihord1  31479  dihjatcclem4  31682
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-rab 2637  df-v 2875  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-sn 3735  df-pr 3736  df-op 3738  df-br 4126
  Copyright terms: Public domain W3C validator