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

Theorem breqtrd 4196
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 4184 . 2  |-  ( ph  ->  ( A R B  <-> 
A R C ) )
41, 3mpbid 202 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   class class class wbr 4172
This theorem is referenced by:  breqtrrd  4198  syl5breq  4207  domunsn  7216  mapdom2  7237  phplem4  7248  wemaplem2  7472  infdifsn  7567  cantnff  7585  infxpenlem  7851  pwcda1  8030  pwcdadom  8052  infmap2  8054  ssfin4  8146  canthp1lem1  8483  nqereq  8768  ltexnq  8808  ltbtwnnq  8811  add20  9496  mullt0  9503  ltm1  9806  recgt0  9810  prodgt0  9811  prodge0  9813  ltmul1a  9815  recp1lt1  9864  recreclt  9865  ledivp1  9868  ledivp1i  9892  ltdivp1i  9893  ltaddrp2d  10634  xleadd1a  10788  xov1plusxeqvd  10997  fz01en  11035  fladdz  11182  flhalf  11186  fldiv  11196  modsubdir  11240  fzen2  11263  serle  11333  ltexp2a  11386  leexp2a  11390  exple1  11394  expubnd  11395  bernneq  11460  expmulnbnd  11466  discr1  11470  discr  11471  faclbnd6  11545  hashfz  11647  hashfun  11655  seqcoll  11667  sqeqd  11926  sqrlem7  12009  sqrge0  12018  sqrneglem  12027  abslt  12073  absle  12074  abstri  12089  rlimge0  12330  reccn2  12345  climaddc2  12384  isercolllem1  12413  caucvgrlem  12421  summolem2a  12464  isumge0  12505  fsumle  12533  fsumlt  12534  o1fsum  12547  supcvg  12590  expcnv  12598  geolim  12602  geolim2  12603  georeclim  12604  geo2lim  12607  mertenslem1  12616  mertens  12618  efcllem  12635  ef0lem  12636  efgt0  12659  eftlub  12665  eflt  12673  sinbnd  12736  cosbnd  12737  ef01bndlem  12740  sin01gt0  12746  cos01gt0  12747  sin02gt0  12748  eirrlem  12758  rpnnen2lem11  12779  rpnnen2  12780  ruclem11  12794  dvdssub2  12842  dvdsadd2b  12847  dvdsexp  12860  3dvds  12867  bitsfzolem  12901  bitsinv1lem  12908  bezoutlem4  12996  dvdsgcd  12998  dvdsmulgcd  13009  nn0seqcvgd  13016  prmind2  13045  rpmulgcd2  13060  qredeq  13061  rpdvds  13079  divdenle  13096  hashdvds  13119  phimullem  13123  eulerthlem2  13126  prmdiveq  13130  prmdivdiv  13131  opoe  13140  pythagtriplem4  13148  pythagtriplem10  13149  pythagtriplem19  13162  iserodd  13164  pcpre1  13171  pcadd2  13214  qexpz  13225  expnprm  13226  pockthlem  13228  prmreclem2  13240  prmreclem3  13241  4sqlem7  13267  4sqlem10  13270  4sqlem11  13278  4sqlem12  13279  4sqlem14  13281  4sqlem15  13282  4sqlem16  13283  0ram  13343  ffthiso  14081  latmlej12  14475  divsgrp  14950  pgpfi1  15184  sylow1lem4  15190  sylow1lem5  15191  odcau  15193  pgpfi  15194  pgpssslw  15203  sylow3lem4  15219  sylow3lem6  15221  efgsfo  15326  frgp0  15347  odadd1  15418  odadd2  15419  odadd  15420  gexexlem  15422  lt6abl  15459  dprd2dlem1  15554  dprd2d2  15557  ablfacrplem  15578  ablfacrp  15579  ablfacrp2  15580  ablfac1b  15583  ablfac1eu  15586  pgpfac1lem3a  15589  ablfaclem2  15599  dvdsrid  15711  dvdsrtr  15712  dvdsrneg  15714  unitmulcl  15724  unitgrp  15727  unitnegcl  15741  isdrng2  15800  subrguss  15838  subrgunit  15841  abvsubtri  15878  fidomndrnglem  16321  psrbaglesupp  16388  gzrngunit  16719  prmirredlem  16728  znidomb  16797  psmetsym  18294  psmettri  18295  mettri2  18324  xmetsym  18330  xmettri  18334  prdsxmetlem  18351  xblss2ps  18384  xblss2  18385  blhalf  18388  xmsge0  18446  ngptgp  18630  nrginvrcnlem  18679  nmoeq0  18723  cnmet  18759  blcvx  18782  opnreen  18815  metdcnlem  18820  metdstri  18834  metdsle  18835  metnrmlem1  18842  metnrmlem3  18844  lebnumlem1  18939  pi1inv  19030  cphnmf  19111  ipge0  19114  ipcau2  19144  tchcphlem1  19145  minveclem2  19280  minveclem3  19283  ovolssnul  19336  ovolctb  19339  ovolunnul  19349  ovoliunlem1  19351  ovoliun2  19355  ovoliunnul  19356  ioombl1lem4  19408  uniioombllem3  19430  uniioombllem4  19431  uniioombllem5  19432  uniioombl  19434  volcn  19451  vitalilem2  19454  vitalilem5  19457  itg1lea  19557  mbfi1fseqlem6  19565  mbfi1flimlem  19567  itg2eqa  19590  itg2splitlem  19593  itg2split  19594  itg2monolem1  19595  itg2cnlem2  19607  iblabsr  19674  iblmulc2  19675  dveflem  19816  dvef  19817  dvferm2lem  19823  dvlip  19830  c1liplem1  19833  dveq0  19837  dvlt0  19842  dvivthlem1  19845  lhop1  19851  dvfsumle  19858  dvfsumlem4  19866  dvfsumrlim3  19870  dvfsum2  19871  ftc1a  19874  ftc1lem4  19876  deg1add  19979  ply1divex  20012  ply1rem  20039  fta1glem2  20042  fta1blem  20044  ig1pdvds  20052  plyeq0lem  20082  dgrcolem2  20145  plydivlem4  20166  plyrem  20175  fta1lem  20177  aalioulem3  20204  aaliou2b  20211  aaliou3lem3  20214  aaliou3lem8  20215  ulmcn  20268  ulmdvlem1  20269  itgulm  20277  pserulm  20291  pserdvlem2  20297  abelthlem2  20301  abelthlem5  20304  abelthlem6  20305  abelthlem7  20307  abelthlem8  20308  abelthlem9  20309  sinq12gt0  20368  sinq34lt0t  20370  cosq14gt0  20371  cosq14ge0  20372  efif1olem3  20399  argimgt0  20460  argimlt0  20461  logneg2  20463  logcnlem3  20488  logcnlem4  20489  logtayllem  20503  logtayl2  20506  cxpsqrlem  20546  cxpsqr  20547  cxpaddlelem  20588  abscxpbnd  20590  loglesqr  20595  ang180lem2  20605  atanlogaddlem  20706  atanlogsublem  20708  atantan  20716  atans2  20724  atantayl  20730  leibpi  20735  log2tlbnd  20738  birthdaylem2  20744  birthdaylem3  20745  cxp2limlem  20767  jensenlem2  20779  jensen  20780  logdiflbnd  20786  emcllem2  20788  emcllem4  20790  harmonicbnd4  20802  fsumharmonic  20803  wilthlem3  20806  basellem1  20816  basellem3  20818  basellem4  20819  fsumdvdsdiaglem  20921  dvdsppwf1o  20924  dvdsmulf1o  20932  chteq0  20946  chtub  20949  chpub  20957  logfacubnd  20958  logfaclbnd  20959  logexprlim  20962  perfectlem2  20967  dchrfi  20992  bclbnd  21017  bposlem1  21021  bposlem3  21023  bposlem4  21024  bposlem6  21026  lgslem1  21033  lgsqrlem2  21079  lgsqrlem4  21081  lgseisenlem2  21087  lgsquadlem1  21091  lgsquadlem2  21092  lgsquad2lem1  21095  2sqlem3  21103  2sqlem4  21104  2sqlem8  21109  2sqlem11  21112  chebbnd1lem2  21117  chebbnd1lem3  21118  chtppilimlem1  21120  chpchtlim  21126  vmadivsum  21129  vmadivsumb  21130  rpvmasumlem  21134  dchrisumlem2  21137  dchrmusum2  21141  dchrvmasumlem2  21145  dchrvmasumlem3  21146  dchrisum0flblem2  21156  dchrisum0fno1  21158  dchrisum0re  21160  dchrisum0lem1  21163  dchrisum0lem2a  21164  mudivsum  21177  mulogsumlem  21178  mulog2sumlem2  21182  vmalogdivsum2  21185  selberglem2  21193  selbergb  21196  selberg2b  21199  logdivbnd  21203  selberg3lem1  21204  selberg3lem2  21205  selberg4lem1  21207  pntrmax  21211  pntrlog2bndlem2  21225  pntrlog2bndlem3  21226  pntrlog2bndlem5  21228  pntrlog2bndlem6a  21229  pntrlog2bndlem6  21230  pntrlog2bnd  21231  pntpbnd1a  21232  pntpbnd1  21233  pntpbnd2  21234  pntibndlem1  21236  pntibndlem2  21238  pntlemb  21244  pntlemq  21248  pntlemr  21249  pntlemj  21250  pntlemk  21253  qabvle  21272  padicabvcxp  21279  ostth2lem2  21281  ostth2lem3  21282  ostth2lem4  21283  ostth3  21285  nvge0  22116  smcnlem  22146  nmoub3i  22227  nmoub2i  22228  nmlno0lem  22247  minvecolem2  22330  htthlem  22373  norm3dif2  22606  bcs2  22637  chscllem2  23093  eigposi  23292  nmopub2tALT  23365  nmfnleub2  23382  nmlnop0iALT  23451  riesz1  23521  cnlnadjlem2  23524  nmopcoadji  23557  leopsq  23585  leopmul  23590  leopnmid  23594  nmopleid  23595  opsqrlem6  23601  0leopj  23642  hstle1  23682  strlem3a  23708  mdslmd4i  23789  cvexchlem  23824  cdj1i  23889  le2halvesd  24075  xlt2addrd  24077  xrge0tsmsd  24176  ofldsqr  24193  ofld0le1  24195  metideq  24241  metider  24242  sqsscirc1  24259  esumle  24402  esummono  24403  esumlef  24407  esumcst  24408  aean  24548  dya2ub  24573  dya2icoseg  24580  lgamgulmlem2  24767  lgamgulm2  24773  lgambdd  24774  lgamucov  24775  lgamcvglem  24777  lgamcvg2  24792  gamcvg  24793  subfacval3  24828  sconpht2  24878  sconpi1  24879  rescon  24886  snmlff  24969  sinccvglem  25062  mulge0b  25144  prodmolem2a  25213  faclimlem2  25311  colinearalglem4  25752  axpaschlem  25783  axcontlem7  25813  btwnouttr2  25860  ltflcei  26140  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  volsupnfl  26150  itg2addnclem  26155  itg2addnclem3  26157  iblmulc2nc  26169  bddiblnc  26174  ftc1cnnclem  26177  csbrn  26346  geomcau  26355  bfplem2  26422  rrncmslem  26431  rrnequiv  26434  irrapxlem1  26775  pell1qrgaplem  26826  pell1qrgap  26827  monotoddzzfi  26895  jm2.24nn  26914  congtr  26920  congmul  26922  congsub  26925  fzmaxdif  26936  acongeq  26938  bezoutr1  26941  jm2.20nn  26958  jm2.25  26960  mapfien2  27126  hbtlem4  27198  dgrsub2  27207  mpaaeu  27223  idomsubgmo  27382  dvconstbi  27419  mulltgt0  27560  fmul01  27577  fmul01lt1lem1  27581  fmul01lt1lem2  27582  climrec  27596  climexp  27598  climneg  27603  stoweidlem1  27617  stoweidlem11  27627  stoweidlem13  27629  stoweidlem26  27642  stoweidlem34  27650  stoweidlem38  27654  stoweidlem42  27658  stoweidlem51  27667  stoweidlem59  27675  stirlinglem5  27694  stirlinglem6  27695  stirlinglem7  27696  stirlinglem10  27699  stirlinglem11  27700  stirlinglem12  27701  stirlinglem13  27702  stirlinglem15  27704  lsatcvatlem  29532  islshpcv  29536  atlatmstc  29802  cvlsupr7  29831  cvrval3  29895  cvrval5  29897  cvrexchlem  29901  atcvrj1  29913  cvrat3  29924  cvrat4  29925  atbtwn  29928  1cvratex  29955  hlatexch4  29963  3atlem1  29965  3atlem2  29966  atcvrlln2  30001  atcvrlln  30002  lplnllnneN  30038  llncvrlpln2  30039  4atlem3b  30080  lplncvrlvol2  30097  dalemswapyz  30138  dalemswapyzps  30172  dalem25  30180  dalem39  30193  dalem58  30212  dalem59  30213  lneq2at  30260  lncvrat  30264  dalawlem2  30354  dalawlem3  30355  dalawlem4  30356  dalawlem6  30358  dalawlem9  30361  dalawlem11  30363  dalawlem12  30364  lhpocnle  30498  lhpmcvr3  30507  lhpmcvr5N  30509  lhpmcvr6N  30510  4atexlemunv  30548  4atexlemc  30551  4atexlemex2  30553  lautm  30576  cdlemc2  30674  cdleme5  30722  cdleme11j  30749  cdleme16b  30761  cdlemednpq  30781  cdleme19e  30789  cdleme20i  30799  cdleme22a  30822  cdleme22cN  30824  cdleme22d  30825  cdleme22e  30826  cdleme22eALTN  30827  cdleme22f  30828  cdleme23c  30833  cdleme30a  30860  cdleme35a  30930  cdleme35b  30932  cdleme42h  30964  cdlemeg46rgv  31010  cdlemg8b  31110  cdlemg12e  31129  cdlemg13a  31133  cdlemg17pq  31154  cdlemg18c  31162  cdlemg19  31166  cdlemg21  31168  cdlemg31d  31182  cdlemg33a  31188  tendoid  31255  cdlemk4  31316  cdlemki  31323  cdlemk10  31325  cdlemksv2  31329  cdlemk12  31332  cdlemk14  31336  cdlemk15  31337  cdlemk1u  31341  cdlemk5u  31343  cdlemk12u  31354  cdlemk45  31429  cdlemk48  31432  dia2dimlem1  31547  dia2dimlem2  31548  dia2dimlem3  31549  cdlemm10N  31601  cdlemn2  31678  dihjustlem  31699  dihglbcpreN  31783  dihmeetlem3N  31788
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173
  Copyright terms: Public domain W3C validator