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

Theorem breqtrrd 4051
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 2290 . 2  |-  ( ph  ->  B  =  C )
41, 3breqtrd 4049 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1624   class class class wbr 4025
This theorem is referenced by:  marypha1lem  7182  marypha2  7188  unxpwdom  7299  uncdadom  7793  cdacomen  7803  cdaassen  7804  xpcdaen  7805  onacda  7819  infcdaabs  7828  cfss  7887  tskuni  8401  ltexnq  8595  xrmax1  10499  xrmax2  10500  max1ALT  10510  qbtwnxr  10522  xleadd1a  10568  xlt2add  10575  xlesubadd  10578  xmulgt0  10598  xlemul1a  10603  xov1plusxeqvd  10775  fzctr  10849  modge0  10975  modlt  10976  modid  10988  sermono  11073  seqf1olem1  11080  seqf1olem2  11081  leexp1a  11155  sqgt0  11167  sqge0  11175  nnlesq  11201  expnbnd  11225  expmulnbnd  11228  discr1  11232  facwordi  11297  faclbnd5  11306  hashdom  11356  swrds2  11555  cjmulge0  11626  resqrcl  11734  absge0  11767  sqreulem  11838  amgm2  11848  rlimdm  12020  rlimge0  12050  reccn2  12065  climle  12108  climserle  12131  isercoll2  12137  iseraltlem1  12149  iseralt  12152  isumclim2  12216  isumclim3  12217  isumge0  12224  fsumless  12249  cvgcmp  12269  cvgcmpce  12271  abscvgcvg  12272  isumsup2  12300  isumltss  12302  climcndslem1  12303  climcnds  12305  supcvg  12309  harmonic  12312  expcnv  12317  explecnv  12318  cvgrat  12334  mertenslem1  12335  mertenslem2  12336  efcvg  12361  ege2le3  12366  efaddlem  12369  eftlub  12384  effsumlt  12386  tanhlt1  12435  ef01bndlem  12459  sin02gt0  12467  rpnnen2lem4  12491  ruclem2  12505  ruclem3  12506  ruclem9  12511  iddvdsexp  12547  dvdsadd  12562  dvdsfac  12578  dvdsmod  12580  3dvds  12586  divalglem1  12588  bitsfzo  12621  bitsmod  12622  bitscmp  12624  bitsinv1lem  12627  sadcaddlem  12643  sadadd3  12647  sadaddlem  12652  dvdssqim  12727  dvdsmulgcd  12728  nn0seqcvgd  12735  sqnprm  12772  mulgcddvds  12778  qredeq  12780  isprm6  12783  nonsq  12825  hashdvds  12838  prmdiv  12848  odzdvds  12855  omoe  12860  pythagtriplem4  12867  pcpre1  12890  pcdvdsb  12916  pcz  12928  pcprmpw2  12929  pcaddlem  12931  pcadd  12932  pcadd2  12933  pcmpt  12935  pcmptdvds  12937  fldivp1  12940  pcfaclem  12941  pockthlem  12947  prmreclem1  12958  prmreclem3  12960  prmreclem5  12962  prmreclem6  12963  4sqlem6  12985  4sqlem8  12987  4sqlem11  12997  4sqlem12  12998  4sqlem14  13000  4sqlem16  13002  vdwlem3  13025  vdwlem9  13031  vdwlem10  13032  vdwlem12  13034  ramub1lem2  13069  invfuc  13843  ple1  14145  eqgen  14665  lagsubg  14674  pgpfi  14911  sylow2alem2  14924  sylow2a  14925  sylow3lem4  14936  efgsrel  15038  odadd1  15135  odadd2  15136  gexex  15140  lt6abl  15176  dprd2d2  15274  dmdprdpr  15279  ablfacrp2  15297  ablfac1c  15301  pgpfaclem1  15311  ablfac2  15319  dvdsrmul1  15430  unitmulclb  15442  subrguss  15555  abvres  15599  znfld  16509  znunit  16512  isxmet2d  17887  mettri  17911  xmettri3  17912  mettri3  17913  xmetrtri2  17915  prdsxmetlem  17927  imasdsf1olem  17932  blss2  17954  blss  17967  prdsbl  18032  dscmet  18090  nmge0  18133  nmmtri  18138  nlmvscnlem2  18191  nrginvrcnlem  18196  nmoix  18233  nmoleub  18235  blcvx  18299  xrsxmet  18310  opnreen  18331  xrge0tsms  18334  icopnfcnv  18435  xrhmeo  18439  lebnumii  18459  pcophtb  18522  pi1grplem  18542  nmoleub2lem  18590  ipcau2  18659  tchcphlem1  18660  ipcau  18663  ipcnlem2  18666  minveclem2  18785  minveclem3b  18787  pjthlem1  18796  pjthlem2  18797  ivthlem3  18808  ivth2  18810  ovolfsf  18826  ovolsslem  18838  ovollb2lem  18842  ovollb2  18843  ovolctb  18844  ovolfiniun  18855  ovolicc1  18870  ovolicc2lem4  18874  ovolicc2  18876  nulmbl2  18889  unmbl  18890  ioombl1lem4  18913  uniioombllem4  18936  uniioombllem6  18938  volivth  18957  vitalilem4  18961  itg1ge0  19036  itg1ge0a  19061  itg1lea  19062  itg1climres  19064  mbfi1fseqlem5  19069  itg2ub  19083  itg2seq  19092  itg2uba  19093  itg2splitlem  19098  itg2split  19099  itg2monolem3  19102  itg2mono  19103  itg2i1fseq2  19106  itg2addlem  19108  iblss  19154  itggt0  19191  dvferm2lem  19328  dvlip  19335  dvivthlem1  19350  dvfsumlem2  19369  dvfsumlem3  19370  ftc1lem4  19381  ply1divmo  19516  ply1remlem  19543  fta1glem2  19547  ig1pdvds  19557  plyeq0lem  19587  plydiveu  19673  fta1lem  19682  vieta1lem2  19686  aaliou3lem2  19718  aaliou3lem8  19720  ulmcn  19771  mtest  19776  itgulm  19779  radcnvlem1  19784  radcnvlt1  19789  dvradcnv  19792  pserdvlem2  19799  abelthlem2  19803  abelthlem6  19807  abelthlem7  19809  abelthlem9  19811  tangtx  19868  sinq12gt0  19870  sineq0  19884  cosordlem  19888  tanord  19895  tanregt0  19896  logrnaddcl  19926  logcj  19955  argregt0  19959  argrege0  19960  argimgt0  19961  argimlt0  19962  logimul  19963  logneg2  19964  logdivlti  19966  divlogrlim  19977  logcnlem3  19986  logcnlem4  19987  dvlog2lem  19994  logtayl  20002  rpcxpcl  20018  cxpsqrlem  20044  cxpaddle  20087  isosctrlem1  20113  asinlem3a  20161  asinlem3  20162  asinneg  20177  asinsinlem  20182  asinsin  20183  atanlogaddlem  20204  atanlogadd  20205  atanlogsublem  20206  atanlogsub  20207  atantan  20214  atanbndlem  20216  atantayl  20228  leibpi  20233  birthdaylem3  20243  areaf  20251  cxploglim  20267  jensenlem2  20277  jensen  20278  harmonicbnd4  20299  fsumharmonic  20300  wilthlem2  20302  ftalem1  20305  ftalem2  20306  ftalem5  20309  basellem6  20318  basellem8  20320  basellem9  20321  chtge0  20345  chtublem  20445  logexprlim  20459  perfectlem1  20463  bcmax  20512  bposlem1  20518  bposlem2  20519  bposlem6  20523  bposlem7  20524  lgsdilem2  20565  lgsqrlem4  20578  lgsquadlem1  20588  2sqlem3  20600  2sqlem8  20606  2sqblem  20611  chebbnd1lem2  20614  chtppilimlem1  20617  chtppilim  20619  chto1ub  20620  vmadivsum  20626  rplogsumlem1  20628  rplogsumlem2  20629  dchrisum0lem1a  20630  rpvmasumlem  20631  dchrisumlem1  20633  dchrisumlem2  20634  dchrvmasumlem2  20642  dchrisum0flblem1  20652  dchrisum0flblem2  20653  dchrisum0lem1b  20659  dchrisum0lem1  20660  dchrisum0lem2a  20661  dchrisum0lem3  20663  dchrisum0  20664  mudivsum  20674  mulogsumlem  20675  mulog2sumlem1  20678  mulog2sumlem2  20679  2vmadivsumlem  20684  chpdifbndlem1  20697  selberg3lem1  20701  selberg4lem1  20704  pntrlog2bndlem1  20721  pntrlog2bndlem2  20722  pntrlog2bndlem3  20723  pntrlog2bndlem4  20724  pntpbnd1a  20729  pntpbnd1  20730  pntpbnd2  20731  pntibndlem2  20735  pntibndlem3  20736  pntlemd  20738  pntlemc  20739  pntlemb  20741  pntlemg  20742  pntlemh  20743  pntlemr  20746  pntlemf  20749  pntlemo  20751  abvcxp  20759  ostth2lem1  20762  padicabv  20774  ostth2lem2  20778  ostth2lem3  20779  ostth2lem4  20780  ostth2  20781  ostth3  20782  nvabs  21232  nmooge0  21338  nmoolb  21342  siii  21424  minvecolem2  21447  minvecolem4  21452  minvecolem5  21453  hlipgt0  21486  normge0  21698  normpyc  21718  pjhthlem1  21963  pjige0i  22262  nmoplb  22480  nmfnlb  22497  branmfn  22678  pjssdif2i  22747  stlei  22813  ballotlem5  23052  ballotlemsgt1  23063  ballotlemsel1i  23065  zetacvg  23094  subfaclim  23124  erdszelem7  23133  erdszelem8  23134  cvmliftlem2  23222  umgraex  23280  snmlff  23317  sinccvglem  23410  dvdspw  23507  axdense  23745  axfelem9  23756  axpaschlem  23976  axcontlem8  24007  truni1  24905  cntrset  25002  mslb1  25007  fnejoin1  25717  isbnd3  25908  ssbnd  25912  heiborlem8  25942  bfplem2  25947  rrncmslem  25956  rrnequiv  25959  rrntotbnd  25960  eldioph2lem1  26239  lzenom  26249  irrapxlem1  26307  irrapxlem4  26310  irrapxlem5  26311  pell14qrgt0  26344  pell1qrge1  26355  pell1qrgap  26359  pellfundge  26367  pellfundex  26371  pellfund14  26383  rmspecsqrnq  26391  rmxypos  26434  ltrmynn0  26435  ltrmxnn0  26436  jm2.24nn  26446  jm2.17b  26448  jm2.17c  26449  jm2.24  26450  congadd  26453  congsym  26455  congneg  26456  congid  26458  mzpcong  26459  acongrep  26467  acongeq  26470  jm2.18  26481  jm2.19  26486  jm2.23  26489  jm2.25  26492  jm2.26lem3  26494  jm2.15nn0  26496  jm2.16nn0  26497  jm2.27a  26498  jm2.27c  26500  jm3.1lem1  26510  idomrootle  26911  idomsubgmo  26914  cncmpmax  27103  fmul01  27110  fmul01lt1lem1  27114  climdivf  27138  stoweidlem1  27150  stoweidlem3  27152  stoweidlem16  27165  stoweidlem18  27167  stoweidlem26  27175  stoweidlem36  27185  stoweidlem38  27187  stoweidlem41  27190  stoweidlem42  27191  stoweidlem44  27193  stoweidlem45  27194  stoweidlem48  27197  stoweidlem51  27200  stoweidlem62  27211  wallispilem5  27218  stirlinglem1  27223  stirlinglem8  27230  stirlinglem9  27231  lcv1  28499  lsatcv0eq  28505  lsatcvat3  28510  cvlsupr2  28801  hlatlej2  28833  cvrval4N  28871  cvratlem  28878  atcvr0eq  28883  2atlt  28896  atbtwnex  28905  athgt  28913  1cvrat  28933  ps-1  28934  hlatexch3N  28937  hlatexch4  28938  3atlem2  28941  atcvrlln2  28976  lplnexllnN  29021  4atlem3a  29054  4atlem10b  29062  4atlem11b  29065  4atlem12b  29068  2lplnja  29076  dalemply  29111  dalemsly  29112  dalem1  29116  dalem6  29125  dalem7  29126  dalem-cly  29128  dalem11  29131  dalem12  29132  dalem16  29136  dalem17  29137  dalem38  29167  dalem44  29173  dalem61  29190  lnatexN  29236  lncvrat  29239  lncmp  29240  paddasslem2  29278  dalawlem3  29330  dalawlem6  29333  dalawlem11  29338  lhpmcvr  29480  lhp2atne  29491  lhp2at0ne  29493  lautj  29550  trlval4  29645  cdlemc2  29649  cdlemc5  29652  cdleme3b  29686  cdleme11c  29718  cdleme19a  29760  cdleme20j  29775  cdleme22f  29803  cdleme23c  29808  cdleme26f2ALTN  29821  cdleme26f2  29822  cdleme35fnpq  29906  cdleme48bw  29959  cdlemg10a  30097  cdlemg11b  30099  cdlemg17g  30124  cdlemg18c  30137  cdlemi1  30275  cdlemk52  30411  dia2dimlem1  30522  dihord1  30676  dihjatcclem4  30879
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-br 4026
  Copyright terms: Public domain W3C validator