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

Theorem breqtrrd 4049
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 2288 . 2  |-  ( ph  ->  B  =  C )
41, 3breqtrd 4047 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   class class class wbr 4023
This theorem is referenced by:  marypha1lem  7186  marypha2  7192  unxpwdom  7303  uncdadom  7797  cdacomen  7807  cdaassen  7808  xpcdaen  7809  onacda  7823  infcdaabs  7832  cfss  7891  tskuni  8405  ltexnq  8599  xrmax1  10504  xrmax2  10505  max1ALT  10515  qbtwnxr  10527  xleadd1a  10573  xlt2add  10580  xlesubadd  10583  xmulgt0  10603  xlemul1a  10608  xov1plusxeqvd  10780  fzctr  10854  modge0  10980  modlt  10981  modid  10993  sermono  11078  seqf1olem1  11085  seqf1olem2  11086  leexp1a  11160  sqgt0  11172  sqge0  11180  nnlesq  11206  expnbnd  11230  expmulnbnd  11233  discr1  11237  facwordi  11302  faclbnd5  11311  hashdom  11361  swrds2  11560  cjmulge0  11631  resqrcl  11739  absge0  11772  sqreulem  11843  amgm2  11853  rlimdm  12025  rlimge0  12055  reccn2  12070  climle  12113  climserle  12136  isercoll2  12142  iseraltlem1  12154  iseralt  12157  isumclim2  12221  isumclim3  12222  isumge0  12229  fsumless  12254  cvgcmp  12274  cvgcmpce  12276  abscvgcvg  12277  isumsup2  12305  isumltss  12307  climcndslem1  12308  climcnds  12310  supcvg  12314  harmonic  12317  expcnv  12322  explecnv  12323  cvgrat  12339  mertenslem1  12340  mertenslem2  12341  efcvg  12366  ege2le3  12371  efaddlem  12374  eftlub  12389  effsumlt  12391  tanhlt1  12440  ef01bndlem  12464  sin02gt0  12472  rpnnen2lem4  12496  ruclem2  12510  ruclem3  12511  ruclem9  12516  iddvdsexp  12552  dvdsadd  12567  dvdsfac  12583  dvdsmod  12585  3dvds  12591  divalglem1  12593  bitsfzo  12626  bitsmod  12627  bitscmp  12629  bitsinv1lem  12632  sadcaddlem  12648  sadadd3  12652  sadaddlem  12657  dvdssqim  12732  dvdsmulgcd  12733  nn0seqcvgd  12740  sqnprm  12777  mulgcddvds  12783  qredeq  12785  isprm6  12788  nonsq  12830  hashdvds  12843  prmdiv  12853  odzdvds  12860  omoe  12865  pythagtriplem4  12872  pcpre1  12895  pcdvdsb  12921  pcz  12933  pcprmpw2  12934  pcaddlem  12936  pcadd  12937  pcadd2  12938  pcmpt  12940  pcmptdvds  12942  fldivp1  12945  pcfaclem  12946  pockthlem  12952  prmreclem1  12963  prmreclem3  12965  prmreclem5  12967  prmreclem6  12968  4sqlem6  12990  4sqlem8  12992  4sqlem11  13002  4sqlem12  13003  4sqlem14  13005  4sqlem16  13007  vdwlem3  13030  vdwlem9  13036  vdwlem10  13037  vdwlem12  13039  ramub1lem2  13074  invfuc  13848  ple1  14150  eqgen  14670  lagsubg  14679  pgpfi  14916  sylow2alem2  14929  sylow2a  14930  sylow3lem4  14941  efgsrel  15043  odadd1  15140  odadd2  15141  gexex  15145  lt6abl  15181  dprd2d2  15279  dmdprdpr  15284  ablfacrp2  15302  ablfac1c  15306  pgpfaclem1  15316  ablfac2  15324  dvdsrmul1  15435  unitmulclb  15447  subrguss  15560  abvres  15604  znfld  16514  znunit  16517  isxmet2d  17892  mettri  17916  xmettri3  17917  mettri3  17918  xmetrtri2  17920  prdsxmetlem  17932  imasdsf1olem  17937  blss2  17959  blss  17972  prdsbl  18037  dscmet  18095  nmge0  18138  nmmtri  18143  nlmvscnlem2  18196  nrginvrcnlem  18201  nmoix  18238  nmoleub  18240  blcvx  18304  xrsxmet  18315  opnreen  18336  xrge0tsms  18339  icopnfcnv  18440  xrhmeo  18444  lebnumii  18464  pcophtb  18527  pi1grplem  18547  nmoleub2lem  18595  ipcau2  18664  tchcphlem1  18665  ipcau  18668  ipcnlem2  18671  minveclem2  18790  minveclem3b  18792  pjthlem1  18801  pjthlem2  18802  ivthlem3  18813  ivth2  18815  ovolfsf  18831  ovolsslem  18843  ovollb2lem  18847  ovollb2  18848  ovolctb  18849  ovolfiniun  18860  ovolicc1  18875  ovolicc2lem4  18879  ovolicc2  18881  nulmbl2  18894  unmbl  18895  ioombl1lem4  18918  uniioombllem4  18941  uniioombllem6  18943  volivth  18962  vitalilem4  18966  itg1ge0  19041  itg1ge0a  19066  itg1lea  19067  itg1climres  19069  mbfi1fseqlem5  19074  itg2ub  19088  itg2seq  19097  itg2uba  19098  itg2splitlem  19103  itg2split  19104  itg2monolem3  19107  itg2mono  19108  itg2i1fseq2  19111  itg2addlem  19113  iblss  19159  itggt0  19196  dvferm2lem  19333  dvlip  19340  dvivthlem1  19355  dvfsumlem2  19374  dvfsumlem3  19375  ftc1lem4  19386  ply1divmo  19521  ply1remlem  19548  fta1glem2  19552  ig1pdvds  19562  plyeq0lem  19592  plydiveu  19678  fta1lem  19687  vieta1lem2  19691  aaliou3lem2  19723  aaliou3lem8  19725  ulmcn  19776  mtest  19781  itgulm  19784  radcnvlem1  19789  radcnvlt1  19794  dvradcnv  19797  pserdvlem2  19804  abelthlem2  19808  abelthlem6  19812  abelthlem7  19814  abelthlem9  19816  tangtx  19873  sinq12gt0  19875  sineq0  19889  cosordlem  19893  tanord  19900  tanregt0  19901  logrnaddcl  19931  logcj  19960  argregt0  19964  argrege0  19965  argimgt0  19966  argimlt0  19967  logimul  19968  logneg2  19969  logdivlti  19971  divlogrlim  19982  logcnlem3  19991  logcnlem4  19992  dvlog2lem  19999  logtayl  20007  rpcxpcl  20023  cxpsqrlem  20049  cxpaddle  20092  isosctrlem1  20118  asinlem3a  20166  asinlem3  20167  asinneg  20182  asinsinlem  20187  asinsin  20188  atanlogaddlem  20209  atanlogadd  20210  atanlogsublem  20211  atanlogsub  20212  atantan  20219  atanbndlem  20221  atantayl  20233  leibpi  20238  birthdaylem3  20248  areaf  20256  cxploglim  20272  jensenlem2  20282  jensen  20283  harmonicbnd4  20304  fsumharmonic  20305  wilthlem2  20307  ftalem1  20310  ftalem2  20311  ftalem5  20314  basellem6  20323  basellem8  20325  basellem9  20326  chtge0  20350  chtublem  20450  logexprlim  20464  perfectlem1  20468  bcmax  20517  bposlem1  20523  bposlem2  20524  bposlem6  20528  bposlem7  20529  lgsdilem2  20570  lgsqrlem4  20583  lgsquadlem1  20593  2sqlem3  20605  2sqlem8  20611  2sqblem  20616  chebbnd1lem2  20619  chtppilimlem1  20622  chtppilim  20624  chto1ub  20625  vmadivsum  20631  rplogsumlem1  20633  rplogsumlem2  20634  dchrisum0lem1a  20635  rpvmasumlem  20636  dchrisumlem1  20638  dchrisumlem2  20639  dchrvmasumlem2  20647  dchrisum0flblem1  20657  dchrisum0flblem2  20658  dchrisum0lem1b  20664  dchrisum0lem1  20665  dchrisum0lem2a  20666  dchrisum0lem3  20668  dchrisum0  20669  mudivsum  20679  mulogsumlem  20680  mulog2sumlem1  20683  mulog2sumlem2  20684  2vmadivsumlem  20689  chpdifbndlem1  20702  selberg3lem1  20706  selberg4lem1  20709  pntrlog2bndlem1  20726  pntrlog2bndlem2  20727  pntrlog2bndlem3  20728  pntrlog2bndlem4  20729  pntpbnd1a  20734  pntpbnd1  20735  pntpbnd2  20736  pntibndlem2  20740  pntibndlem3  20741  pntlemd  20743  pntlemc  20744  pntlemb  20746  pntlemg  20747  pntlemh  20748  pntlemr  20751  pntlemf  20754  pntlemo  20756  abvcxp  20764  ostth2lem1  20767  padicabv  20779  ostth2lem2  20783  ostth2lem3  20784  ostth2lem4  20785  ostth2  20786  ostth3  20787  nvabs  21239  nmooge0  21345  nmoolb  21349  siii  21431  minvecolem2  21454  minvecolem4  21459  minvecolem5  21460  hlipgt0  21493  normge0  21705  normpyc  21725  pjhthlem1  21970  pjige0i  22269  nmoplb  22487  nmfnlb  22504  branmfn  22685  pjssdif2i  22754  stlei  22820  ballotlem5  23058  ballotlemsgt1  23069  ballotlemsel1i  23071  eliccelico  23270  elicoelioo  23271  xrge0tsmsd  23382  hashge1  23388  esumcst  23436  esumpcvgval  23446  esumcvg  23454  zetacvg  23689  subfaclim  23719  erdszelem7  23728  erdszelem8  23729  cvmliftlem2  23817  umgraex  23875  snmlff  23912  sinccvglem  24005  dvdspw  24103  nodense  24343  nobndup  24354  axpaschlem  24568  axcontlem8  24599  truni1  25505  cntrset  25602  mslb1  25607  fnejoin1  26317  isbnd3  26508  ssbnd  26512  heiborlem8  26542  bfplem2  26547  rrncmslem  26556  rrnequiv  26559  rrntotbnd  26560  eldioph2lem1  26839  lzenom  26849  irrapxlem1  26907  irrapxlem4  26910  irrapxlem5  26911  pell14qrgt0  26944  pell1qrge1  26955  pell1qrgap  26959  pellfundge  26967  pellfundex  26971  pellfund14  26983  rmspecsqrnq  26991  rmxypos  27034  ltrmynn0  27035  ltrmxnn0  27036  jm2.24nn  27046  jm2.17b  27048  jm2.17c  27049  jm2.24  27050  congadd  27053  congsym  27055  congneg  27056  congid  27058  mzpcong  27059  acongrep  27067  acongeq  27070  jm2.18  27081  jm2.19  27086  jm2.23  27089  jm2.25  27092  jm2.26lem3  27094  jm2.15nn0  27096  jm2.16nn0  27097  jm2.27a  27098  jm2.27c  27100  jm3.1lem1  27110  idomrootle  27511  idomsubgmo  27514  cncmpmax  27703  fmul01  27710  fmul01lt1lem1  27714  climdivf  27738  stoweidlem1  27750  stoweidlem3  27752  stoweidlem16  27765  stoweidlem18  27767  stoweidlem26  27775  stoweidlem36  27785  stoweidlem38  27787  stoweidlem41  27790  stoweidlem42  27791  stoweidlem44  27793  stoweidlem45  27794  stoweidlem48  27797  stoweidlem51  27800  stoweidlem62  27811  wallispilem5  27818  stirlinglem1  27823  stirlinglem8  27830  stirlinglem9  27831  lcv1  29231  lsatcv0eq  29237  lsatcvat3  29242  cvlsupr2  29533  hlatlej2  29565  cvrval4N  29603  cvratlem  29610  atcvr0eq  29615  2atlt  29628  atbtwnex  29637  athgt  29645  1cvrat  29665  ps-1  29666  hlatexch3N  29669  hlatexch4  29670  3atlem2  29673  atcvrlln2  29708  lplnexllnN  29753  4atlem3a  29786  4atlem10b  29794  4atlem11b  29797  4atlem12b  29800  2lplnja  29808  dalemply  29843  dalemsly  29844  dalem1  29848  dalem6  29857  dalem7  29858  dalem-cly  29860  dalem11  29863  dalem12  29864  dalem16  29868  dalem17  29869  dalem38  29899  dalem44  29905  dalem61  29922  lnatexN  29968  lncvrat  29971  lncmp  29972  paddasslem2  30010  dalawlem3  30062  dalawlem6  30065  dalawlem11  30070  lhpmcvr  30212  lhp2atne  30223  lhp2at0ne  30225  lautj  30282  trlval4  30377  cdlemc2  30381  cdlemc5  30384  cdleme3b  30418  cdleme11c  30450  cdleme19a  30492  cdleme20j  30507  cdleme22f  30535  cdleme23c  30540  cdleme26f2ALTN  30553  cdleme26f2  30554  cdleme35fnpq  30638  cdleme48bw  30691  cdlemg10a  30829  cdlemg11b  30831  cdlemg17g  30856  cdlemg18c  30869  cdlemi1  31007  cdlemk52  31143  dia2dimlem1  31254  dihord1  31408  dihjatcclem4  31611
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024
  Copyright terms: Public domain W3C validator