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

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

Proof of Theorem breqtrd
StepHypRef Expression
1 breqtrd.1 . 2  |-  ( ph  ->  A R B )
2 breqtrd.2 . . 3  |-  ( ph  ->  B  =  C )
32breq2d 4035 . 2  |-  ( ph  ->  ( A R B  <-> 
A R C ) )
41, 3mpbid 201 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:  breqtrrd  4049  syl5breq  4058  domunsn  7011  mapdom2  7032  phplem4  7043  wemaplem2  7262  infdifsn  7357  cantnff  7375  infxpenlem  7641  pwcda1  7820  pwcdadom  7842  infmap2  7844  ssfin4  7936  canthp1lem1  8274  nqereq  8559  ltexnq  8599  ltbtwnnq  8602  add20  9286  mullt0  9293  ltm1  9596  recgt0  9600  prodgt0  9601  prodge0  9603  ltmul1a  9605  recp1lt1  9654  recreclt  9655  ledivp1  9658  ledivp1i  9682  ltdivp1i  9683  ltaddrp2d  10420  xleadd1a  10573  xov1plusxeqvd  10780  fz01en  10818  fladdz  10950  flhalf  10954  fldiv  10964  modsubdir  11008  fzen2  11031  serle  11101  ltexp2a  11153  leexp2a  11157  exple1  11161  expubnd  11162  bernneq  11227  expmulnbnd  11233  discr1  11237  discr  11238  faclbnd6  11312  hashfz  11381  hashfun  11389  seqcoll  11401  sqeqd  11651  sqrlem7  11734  sqrge0  11743  sqrneglem  11752  abslt  11798  absle  11799  abstri  11814  rlimge0  12055  reccn2  12070  climaddc2  12109  isercolllem1  12138  caucvgrlem  12145  summolem2a  12188  isumge0  12229  fsumle  12257  fsumlt  12258  o1fsum  12271  supcvg  12314  expcnv  12322  geolim  12326  geolim2  12327  georeclim  12328  geo2lim  12331  mertenslem1  12340  mertens  12342  efcllem  12359  ef0lem  12360  efgt0  12383  eftlub  12389  eflt  12397  sinbnd  12460  cosbnd  12461  ef01bndlem  12464  sin01gt0  12470  cos01gt0  12471  sin02gt0  12472  eirrlem  12482  rpnnen2lem11  12503  rpnnen2  12504  ruclem11  12518  dvdssub2  12566  dvdsadd2b  12571  dvdsexp  12584  3dvds  12591  bitsfzolem  12625  bitscmp  12629  bitsinv1lem  12632  bezoutlem4  12720  dvdsgcd  12722  dvdsmulgcd  12733  nn0seqcvgd  12740  prmind2  12769  rpmulgcd2  12784  qredeq  12785  rpdvds  12803  divdenle  12820  hashdvds  12843  phimullem  12847  eulerthlem2  12850  prmdiveq  12854  prmdivdiv  12855  opoe  12864  pythagtriplem4  12872  pythagtriplem10  12873  pythagtriplem19  12886  iserodd  12888  pcpre1  12895  pcadd2  12938  qexpz  12949  expnprm  12950  pockthlem  12952  prmreclem2  12964  prmreclem3  12965  4sqlem7  12991  4sqlem10  12994  4sqlem11  13002  4sqlem12  13003  4sqlem14  13005  4sqlem15  13006  4sqlem16  13007  0ram  13067  ffthiso  13803  latmlej12  14197  divsgrp  14672  pgpfi1  14906  sylow1lem4  14912  sylow1lem5  14913  odcau  14915  pgpfi  14916  pgpssslw  14925  sylow3lem4  14941  sylow3lem6  14943  efgsfo  15048  frgp0  15069  odadd1  15140  odadd2  15141  odadd  15142  gexexlem  15144  lt6abl  15181  dprd2dlem1  15276  dprd2d2  15279  ablfacrplem  15300  ablfacrp  15301  ablfacrp2  15302  ablfac1b  15305  ablfac1eu  15308  pgpfac1lem3a  15311  ablfaclem2  15321  dvdsrid  15433  dvdsrtr  15434  dvdsrneg  15436  unitmulcl  15446  unitgrp  15449  unitnegcl  15463  isdrng2  15522  subrguss  15560  subrgunit  15563  abvsubtri  15600  fidomndrnglem  16047  psrbaglesupp  16114  gzrngunit  16437  prmirredlem  16446  znidomb  16515  mettri2  17906  xmetsym  17912  xmettri  17915  prdsxmetlem  17932  xblss2  17958  blhalf  17960  xmsge0  18009  ngptgp  18152  nrginvrcnlem  18201  nmoeq0  18245  cnmet  18281  blcvx  18304  opnreen  18336  metdcnlem  18341  metdstri  18355  metdsle  18356  metnrmlem1  18363  metnrmlem3  18365  lebnumlem1  18459  pi1inv  18550  cphnmf  18631  ipge0  18634  ipcau2  18664  tchcphlem1  18665  minveclem2  18790  minveclem3  18793  ovolssnul  18846  ovolctb  18849  ovolunnul  18859  ovoliunlem1  18861  ovoliun2  18865  ovoliunnul  18866  ioombl1lem4  18918  uniioombllem3  18940  uniioombllem4  18941  uniioombllem5  18942  uniioombl  18944  volcn  18961  vitalilem2  18964  vitalilem5  18967  itg1lea  19067  mbfi1fseqlem6  19075  mbfi1flimlem  19077  itg2eqa  19100  itg2splitlem  19103  itg2split  19104  itg2monolem1  19105  itg2cnlem2  19117  iblabsr  19184  iblmulc2  19185  dveflem  19326  dvef  19327  dvferm2lem  19333  dvlip  19340  c1liplem1  19343  dveq0  19347  dvlt0  19352  dvivthlem1  19355  lhop1  19361  dvfsumle  19368  dvfsumlem4  19376  dvfsumrlim3  19380  dvfsum2  19381  ftc1a  19384  ftc1lem4  19386  deg1add  19489  ply1divex  19522  ply1rem  19549  fta1glem2  19552  fta1blem  19554  ig1pdvds  19562  plyeq0lem  19592  dgrcolem2  19655  plydivlem4  19676  plyrem  19685  fta1lem  19687  aalioulem3  19714  aaliou2b  19721  aaliou3lem3  19724  aaliou3lem8  19725  ulmcn  19776  ulmdvlem1  19777  itgulm  19784  pserulm  19798  pserdvlem2  19804  abelthlem2  19808  abelthlem5  19811  abelthlem6  19812  abelthlem7  19814  abelthlem8  19815  abelthlem9  19816  sinq12gt0  19875  sinq34lt0t  19877  cosq14gt0  19878  cosq14ge0  19879  efif1olem3  19906  argimgt0  19966  argimlt0  19967  logneg2  19969  logcnlem3  19991  logcnlem4  19992  logtayllem  20006  logtayl2  20009  cxpsqrlem  20049  cxpsqr  20050  cxpaddlelem  20091  abscxpbnd  20093  loglesqr  20098  ang180lem2  20108  atanlogaddlem  20209  atanlogsublem  20211  atantan  20219  atans2  20227  atantayl  20233  leibpi  20238  log2tlbnd  20241  birthdaylem2  20247  birthdaylem3  20248  cxp2limlem  20270  jensenlem2  20282  jensen  20283  emcllem2  20290  emcllem4  20292  harmonicbnd4  20304  fsumharmonic  20305  wilthlem3  20308  basellem1  20318  basellem3  20320  basellem4  20321  fsumdvdsdiaglem  20423  dvdsppwf1o  20426  dvdsmulf1o  20434  chteq0  20448  chtub  20451  chpub  20459  logfacubnd  20460  logfaclbnd  20461  logexprlim  20464  perfectlem2  20469  dchrfi  20494  bclbnd  20519  bposlem1  20523  bposlem3  20525  bposlem4  20526  bposlem6  20528  lgslem1  20535  lgsqrlem2  20581  lgsqrlem4  20583  lgseisenlem2  20589  lgsquadlem1  20593  lgsquadlem2  20594  lgsquad2lem1  20597  2sqlem3  20605  2sqlem4  20606  2sqlem8  20611  2sqlem11  20614  chebbnd1lem2  20619  chebbnd1lem3  20620  chtppilimlem1  20622  chpchtlim  20628  vmadivsum  20631  vmadivsumb  20632  rpvmasumlem  20636  dchrisumlem2  20639  dchrmusum2  20643  dchrvmasumlem2  20647  dchrvmasumlem3  20648  dchrisum0flblem2  20658  dchrisum0fno1  20660  dchrisum0re  20662  dchrisum0lem1  20665  dchrisum0lem2a  20666  mudivsum  20679  mulogsumlem  20680  mulog2sumlem2  20684  vmalogdivsum2  20687  selberglem2  20695  selbergb  20698  selberg2b  20701  logdivbnd  20705  selberg3lem1  20706  selberg3lem2  20707  selberg4lem1  20709  pntrmax  20713  pntrlog2bndlem2  20727  pntrlog2bndlem3  20728  pntrlog2bndlem5  20730  pntrlog2bndlem6a  20731  pntrlog2bndlem6  20732  pntrlog2bnd  20733  pntpbnd1a  20734  pntpbnd1  20735  pntpbnd2  20736  pntibndlem1  20738  pntibndlem2  20740  pntlemb  20746  pntlemq  20750  pntlemr  20751  pntlemj  20752  pntlemk  20755  qabvle  20774  padicabvcxp  20781  ostth2lem2  20783  ostth2lem3  20784  ostth2lem4  20785  ostth3  20787  nvge0  21240  smcnlem  21270  nmoub3i  21351  nmoub2i  21352  nmlno0lem  21371  minvecolem2  21454  htthlem  21497  norm3dif2  21730  bcs2  21761  chscllem2  22217  eigposi  22416  nmopub2tALT  22489  nmfnleub2  22506  nmlnop0iALT  22575  riesz1  22645  cnlnadjlem2  22648  nmopcoadji  22681  leopsq  22709  leopmul  22714  leopnmid  22718  nmopleid  22719  opsqrlem6  22725  0leopj  22766  hstle1  22806  strlem3a  22832  mdslmd4i  22913  cvexchlem  22948  cdj1i  23013  sqsscirc1  23292  xrge0tsmsd  23382  esumle  23433  esumlef  23435  esumcst  23436  dya2ub  23575  dya2iocseg  23579  subfacval3  23720  sconpht2  23769  sconpi1  23770  rescon  23777  snmlff  23912  sinccvglem  24005  mulge0b  24086  colinearalglem4  24537  axpaschlem  24568  axcontlem7  24598  btwnouttr2  24645  cntrset  25602  msra3  25609  csbrn  26462  geomcau  26475  bfplem2  26547  rrncmslem  26556  rrnequiv  26559  irrapxlem1  26907  pell1qrgaplem  26958  pell1qrgap  26959  monotoddzzfi  27027  jm2.24nn  27046  congtr  27052  congmul  27054  congsub  27057  fzmaxdif  27068  acongeq  27070  bezoutr1  27073  jm2.20nn  27090  jm2.25  27092  mapfien2  27258  hbtlem4  27330  dgrsub2  27339  mpaaeu  27355  idomsubgmo  27514  dvconstbi  27551  mulltgt0  27693  fmul01  27710  fmul01lt1lem1  27714  fmul01lt1lem2  27715  climrec  27729  climexp  27731  climneg  27736  stoweidlem1  27750  stoweidlem11  27760  stoweidlem13  27762  stoweidlem24  27773  stoweidlem26  27775  stoweidlem34  27783  stoweidlem38  27787  stoweidlem42  27791  stoweidlem51  27800  stoweidlem59  27808  wallispilem5  27818  wallispi2lem1  27820  wallispi2  27822  stirlinglem1  27823  stirlinglem5  27827  stirlinglem6  27828  stirlinglem7  27829  stirlinglem10  27832  stirlinglem11  27833  stirlinglem12  27834  stirlinglem13  27835  stirlinglem15  27837  lsatcvatlem  29239  islshpcv  29243  atlatmstc  29509  cvlsupr7  29538  cvrval3  29602  cvrval5  29604  cvrexchlem  29608  atcvrj1  29620  cvrat3  29631  cvrat4  29632  atbtwn  29635  1cvratex  29662  hlatexch4  29670  3atlem1  29672  3atlem2  29673  atcvrlln2  29708  atcvrlln  29709  lplnllnneN  29745  llncvrlpln2  29746  4atlem3b  29787  lplncvrlvol2  29804  dalemswapyz  29845  dalemswapyzps  29879  dalem25  29887  dalem39  29900  dalem58  29919  dalem59  29920  lneq2at  29967  lncvrat  29971  dalawlem2  30061  dalawlem3  30062  dalawlem4  30063  dalawlem6  30065  dalawlem9  30068  dalawlem11  30070  dalawlem12  30071  lhpocnle  30205  lhpmcvr3  30214  lhpmcvr5N  30216  lhpmcvr6N  30217  4atexlemunv  30255  4atexlemc  30258  4atexlemex2  30260  lautm  30283  cdlemc2  30381  cdleme5  30429  cdleme11j  30456  cdleme16b  30468  cdlemednpq  30488  cdleme19e  30496  cdleme20i  30506  cdleme22a  30529  cdleme22cN  30531  cdleme22d  30532  cdleme22e  30533  cdleme22eALTN  30534  cdleme22f  30535  cdleme23c  30540  cdleme30a  30567  cdleme35a  30637  cdleme35b  30639  cdleme42h  30671  cdlemeg46rgv  30717  cdlemg8b  30817  cdlemg12e  30836  cdlemg13a  30840  cdlemg17pq  30861  cdlemg18c  30869  cdlemg19  30873  cdlemg21  30875  cdlemg31d  30889  cdlemg33a  30895  tendoid  30962  cdlemk4  31023  cdlemki  31030  cdlemk10  31032  cdlemksv2  31036  cdlemk12  31039  cdlemk14  31043  cdlemk15  31044  cdlemk1u  31048  cdlemk5u  31050  cdlemk12u  31061  cdlemk45  31136  cdlemk48  31139  dia2dimlem1  31254  dia2dimlem2  31255  dia2dimlem3  31256  cdlemm10N  31308  cdlemn2  31385  dihjustlem  31406  dihglbcpreN  31490  dihmeetlem3N  31495
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