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

Theorem breqtrd 4149
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 4137 . 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 1647   class class class wbr 4125
This theorem is referenced by:  breqtrrd  4151  syl5breq  4160  domunsn  7154  mapdom2  7175  phplem4  7186  wemaplem2  7409  infdifsn  7504  cantnff  7522  infxpenlem  7788  pwcda1  7967  pwcdadom  7989  infmap2  7991  ssfin4  8083  canthp1lem1  8421  nqereq  8706  ltexnq  8746  ltbtwnnq  8749  add20  9433  mullt0  9440  ltm1  9743  recgt0  9747  prodgt0  9748  prodge0  9750  ltmul1a  9752  recp1lt1  9801  recreclt  9802  ledivp1  9805  ledivp1i  9829  ltdivp1i  9830  ltaddrp2d  10571  xleadd1a  10725  xov1plusxeqvd  10933  fz01en  10971  fladdz  11114  flhalf  11118  fldiv  11128  modsubdir  11172  fzen2  11195  serle  11265  ltexp2a  11318  leexp2a  11322  exple1  11326  expubnd  11327  bernneq  11392  expmulnbnd  11398  discr1  11402  discr  11403  faclbnd6  11477  hashfz  11579  hashfun  11587  seqcoll  11599  sqeqd  11858  sqrlem7  11941  sqrge0  11950  sqrneglem  11959  abslt  12005  absle  12006  abstri  12021  rlimge0  12262  reccn2  12277  climaddc2  12316  isercolllem1  12345  caucvgrlem  12353  summolem2a  12396  isumge0  12437  fsumle  12465  fsumlt  12466  o1fsum  12479  supcvg  12522  expcnv  12530  geolim  12534  geolim2  12535  georeclim  12536  geo2lim  12539  mertenslem1  12548  mertens  12550  efcllem  12567  ef0lem  12568  efgt0  12591  eftlub  12597  eflt  12605  sinbnd  12668  cosbnd  12669  ef01bndlem  12672  sin01gt0  12678  cos01gt0  12679  sin02gt0  12680  eirrlem  12690  rpnnen2lem11  12711  rpnnen2  12712  ruclem11  12726  dvdssub2  12774  dvdsadd2b  12779  dvdsexp  12792  3dvds  12799  bitsfzolem  12833  bitscmp  12837  bitsinv1lem  12840  bezoutlem4  12928  dvdsgcd  12930  dvdsmulgcd  12941  nn0seqcvgd  12948  prmind2  12977  rpmulgcd2  12992  qredeq  12993  rpdvds  13011  divdenle  13028  hashdvds  13051  phimullem  13055  eulerthlem2  13058  prmdiveq  13062  prmdivdiv  13063  opoe  13072  pythagtriplem4  13080  pythagtriplem10  13081  pythagtriplem19  13094  iserodd  13096  pcpre1  13103  pcadd2  13146  qexpz  13157  expnprm  13158  pockthlem  13160  prmreclem2  13172  prmreclem3  13173  4sqlem7  13199  4sqlem10  13202  4sqlem11  13210  4sqlem12  13211  4sqlem14  13213  4sqlem15  13214  4sqlem16  13215  0ram  13275  ffthiso  14013  latmlej12  14407  divsgrp  14882  pgpfi1  15116  sylow1lem4  15122  sylow1lem5  15123  odcau  15125  pgpfi  15126  pgpssslw  15135  sylow3lem4  15151  sylow3lem6  15153  efgsfo  15258  frgp0  15279  odadd1  15350  odadd2  15351  odadd  15352  gexexlem  15354  lt6abl  15391  dprd2dlem1  15486  dprd2d2  15489  ablfacrplem  15510  ablfacrp  15511  ablfacrp2  15512  ablfac1b  15515  ablfac1eu  15518  pgpfac1lem3a  15521  ablfaclem2  15531  dvdsrid  15643  dvdsrtr  15644  dvdsrneg  15646  unitmulcl  15656  unitgrp  15659  unitnegcl  15673  isdrng2  15732  subrguss  15770  subrgunit  15773  abvsubtri  15810  fidomndrnglem  16257  psrbaglesupp  16324  gzrngunit  16654  prmirredlem  16663  znidomb  16732  mettri2  18119  xmetsym  18125  xmettri  18128  prdsxmetlem  18145  xblss2  18171  blhalf  18173  xmsge0  18222  ngptgp  18365  nrginvrcnlem  18414  nmoeq0  18458  cnmet  18494  blcvx  18517  opnreen  18550  metdcnlem  18555  metdstri  18569  metdsle  18570  metnrmlem1  18577  metnrmlem3  18579  lebnumlem1  18674  pi1inv  18765  cphnmf  18846  ipge0  18849  ipcau2  18879  tchcphlem1  18880  minveclem2  19005  minveclem3  19008  ovolssnul  19061  ovolctb  19064  ovolunnul  19074  ovoliunlem1  19076  ovoliun2  19080  ovoliunnul  19081  ioombl1lem4  19133  uniioombllem3  19155  uniioombllem4  19156  uniioombllem5  19157  uniioombl  19159  volcn  19176  vitalilem2  19179  vitalilem5  19182  itg1lea  19282  mbfi1fseqlem6  19290  mbfi1flimlem  19292  itg2eqa  19315  itg2splitlem  19318  itg2split  19319  itg2monolem1  19320  itg2cnlem2  19332  iblabsr  19399  iblmulc2  19400  dveflem  19541  dvef  19542  dvferm2lem  19548  dvlip  19555  c1liplem1  19558  dveq0  19562  dvlt0  19567  dvivthlem1  19570  lhop1  19576  dvfsumle  19583  dvfsumlem4  19591  dvfsumrlim3  19595  dvfsum2  19596  ftc1a  19599  ftc1lem4  19601  deg1add  19704  ply1divex  19737  ply1rem  19764  fta1glem2  19767  fta1blem  19769  ig1pdvds  19777  plyeq0lem  19807  dgrcolem2  19870  plydivlem4  19891  plyrem  19900  fta1lem  19902  aalioulem3  19929  aaliou2b  19936  aaliou3lem3  19939  aaliou3lem8  19940  ulmcn  19993  ulmdvlem1  19994  itgulm  20002  pserulm  20016  pserdvlem2  20022  abelthlem2  20026  abelthlem5  20029  abelthlem6  20030  abelthlem7  20032  abelthlem8  20033  abelthlem9  20034  sinq12gt0  20093  sinq34lt0t  20095  cosq14gt0  20096  cosq14ge0  20097  efif1olem3  20124  argimgt0  20185  argimlt0  20186  logneg2  20188  logcnlem3  20213  logcnlem4  20214  logtayllem  20228  logtayl2  20231  cxpsqrlem  20271  cxpsqr  20272  cxpaddlelem  20313  abscxpbnd  20315  loglesqr  20320  ang180lem2  20330  atanlogaddlem  20431  atanlogsublem  20433  atantan  20441  atans2  20449  atantayl  20455  leibpi  20460  log2tlbnd  20463  birthdaylem2  20469  birthdaylem3  20470  cxp2limlem  20492  jensenlem2  20504  jensen  20505  logdiflbnd  20511  emcllem2  20513  emcllem4  20515  harmonicbnd4  20527  fsumharmonic  20528  wilthlem3  20531  basellem1  20541  basellem3  20543  basellem4  20544  fsumdvdsdiaglem  20646  dvdsppwf1o  20649  dvdsmulf1o  20657  chteq0  20671  chtub  20674  chpub  20682  logfacubnd  20683  logfaclbnd  20684  logexprlim  20687  perfectlem2  20692  dchrfi  20717  bclbnd  20742  bposlem1  20746  bposlem3  20748  bposlem4  20749  bposlem6  20751  lgslem1  20758  lgsqrlem2  20804  lgsqrlem4  20806  lgseisenlem2  20812  lgsquadlem1  20816  lgsquadlem2  20817  lgsquad2lem1  20820  2sqlem3  20828  2sqlem4  20829  2sqlem8  20834  2sqlem11  20837  chebbnd1lem2  20842  chebbnd1lem3  20843  chtppilimlem1  20845  chpchtlim  20851  vmadivsum  20854  vmadivsumb  20855  rpvmasumlem  20859  dchrisumlem2  20862  dchrmusum2  20866  dchrvmasumlem2  20870  dchrvmasumlem3  20871  dchrisum0flblem2  20881  dchrisum0fno1  20883  dchrisum0re  20885  dchrisum0lem1  20888  dchrisum0lem2a  20889  mudivsum  20902  mulogsumlem  20903  mulog2sumlem2  20907  vmalogdivsum2  20910  selberglem2  20918  selbergb  20921  selberg2b  20924  logdivbnd  20928  selberg3lem1  20929  selberg3lem2  20930  selberg4lem1  20932  pntrmax  20936  pntrlog2bndlem2  20950  pntrlog2bndlem3  20951  pntrlog2bndlem5  20953  pntrlog2bndlem6a  20954  pntrlog2bndlem6  20955  pntrlog2bnd  20956  pntpbnd1a  20957  pntpbnd1  20958  pntpbnd2  20959  pntibndlem1  20961  pntibndlem2  20963  pntlemb  20969  pntlemq  20973  pntlemr  20974  pntlemj  20975  pntlemk  20978  qabvle  20997  padicabvcxp  21004  ostth2lem2  21006  ostth2lem3  21007  ostth2lem4  21008  ostth3  21010  nvge0  21553  smcnlem  21583  nmoub3i  21664  nmoub2i  21665  nmlno0lem  21684  minvecolem2  21767  htthlem  21810  norm3dif2  22043  bcs2  22074  chscllem2  22530  eigposi  22729  nmopub2tALT  22802  nmfnleub2  22819  nmlnop0iALT  22888  riesz1  22958  cnlnadjlem2  22961  nmopcoadji  22994  leopsq  23022  leopmul  23027  leopnmid  23031  nmopleid  23032  opsqrlem6  23038  0leopj  23079  hstle1  23119  strlem3a  23145  mdslmd4i  23226  cvexchlem  23261  cdj1i  23326  le2halvesd  23522  xrge0tsmsd  23614  sqsscirc1  23661  esumle  23914  esummono  23915  esumlef  23919  esumcst  23920  aean  24058  dya2ub  24083  dya2icoseg  24090  lgamgulmlem2  24262  lgamgulm2  24268  lgambdd  24269  lgamucov  24270  lgamcvglem  24272  lgamcvg2  24287  gamcvg  24288  subfacval3  24323  sconpht2  24372  sconpi1  24373  rescon  24380  snmlff  24499  sinccvglem  24592  mulge0b  24675  prodmolem2a  24744  faclimlem2  24838  colinearalglem4  25279  axpaschlem  25310  axcontlem7  25340  btwnouttr2  25387  ltflcei  25668  volsupnfl  25674  itg2addnclem  25675  itg2addnc  25677  iblmulc2nc  25688  bddiblnc  25693  ftc1cnnclem  25696  csbrn  25969  geomcau  25982  bfplem2  26053  rrncmslem  26062  rrnequiv  26065  irrapxlem1  26413  pell1qrgaplem  26464  pell1qrgap  26465  monotoddzzfi  26533  jm2.24nn  26552  congtr  26558  congmul  26560  congsub  26563  fzmaxdif  26574  acongeq  26576  bezoutr1  26579  jm2.20nn  26596  jm2.25  26598  mapfien2  26764  hbtlem4  26836  dgrsub2  26845  mpaaeu  26861  idomsubgmo  27020  dvconstbi  27057  mulltgt0  27199  fmul01  27216  fmul01lt1lem1  27220  fmul01lt1lem2  27221  climrec  27235  climexp  27237  climneg  27242  stoweidlem1  27256  stoweidlem11  27266  stoweidlem13  27268  stoweidlem24  27279  stoweidlem26  27281  stoweidlem34  27289  stoweidlem38  27293  stoweidlem42  27297  stoweidlem51  27306  stoweidlem59  27314  wallispilem5  27324  wallispi2lem1  27326  wallispi2  27328  stirlinglem1  27329  stirlinglem5  27333  stirlinglem6  27334  stirlinglem7  27335  stirlinglem10  27338  stirlinglem11  27339  stirlinglem12  27340  stirlinglem13  27341  stirlinglem15  27343  lsatcvatlem  29310  islshpcv  29314  atlatmstc  29580  cvlsupr7  29609  cvrval3  29673  cvrval5  29675  cvrexchlem  29679  atcvrj1  29691  cvrat3  29702  cvrat4  29703  atbtwn  29706  1cvratex  29733  hlatexch4  29741  3atlem1  29743  3atlem2  29744  atcvrlln2  29779  atcvrlln  29780  lplnllnneN  29816  llncvrlpln2  29817  4atlem3b  29858  lplncvrlvol2  29875  dalemswapyz  29916  dalemswapyzps  29950  dalem25  29958  dalem39  29971  dalem58  29990  dalem59  29991  lneq2at  30038  lncvrat  30042  dalawlem2  30132  dalawlem3  30133  dalawlem4  30134  dalawlem6  30136  dalawlem9  30139  dalawlem11  30141  dalawlem12  30142  lhpocnle  30276  lhpmcvr3  30285  lhpmcvr5N  30287  lhpmcvr6N  30288  4atexlemunv  30326  4atexlemc  30329  4atexlemex2  30331  lautm  30354  cdlemc2  30452  cdleme5  30500  cdleme11j  30527  cdleme16b  30539  cdlemednpq  30559  cdleme19e  30567  cdleme20i  30577  cdleme22a  30600  cdleme22cN  30602  cdleme22d  30603  cdleme22e  30604  cdleme22eALTN  30605  cdleme22f  30606  cdleme23c  30611  cdleme30a  30638  cdleme35a  30708  cdleme35b  30710  cdleme42h  30742  cdlemeg46rgv  30788  cdlemg8b  30888  cdlemg12e  30907  cdlemg13a  30911  cdlemg17pq  30932  cdlemg18c  30940  cdlemg19  30944  cdlemg21  30946  cdlemg31d  30960  cdlemg33a  30966  tendoid  31033  cdlemk4  31094  cdlemki  31101  cdlemk10  31103  cdlemksv2  31107  cdlemk12  31110  cdlemk14  31114  cdlemk15  31115  cdlemk1u  31119  cdlemk5u  31121  cdlemk12u  31132  cdlemk45  31207  cdlemk48  31210  dia2dimlem1  31325  dia2dimlem2  31326  dia2dimlem3  31327  cdlemm10N  31379  cdlemn2  31456  dihjustlem  31477  dihglbcpreN  31561  dihmeetlem3N  31566
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