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

Theorem breqtrd 4177
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 4165 . 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 4153
This theorem is referenced by:  breqtrrd  4179  syl5breq  4188  domunsn  7193  mapdom2  7214  phplem4  7225  wemaplem2  7449  infdifsn  7544  cantnff  7562  infxpenlem  7828  pwcda1  8007  pwcdadom  8029  infmap2  8031  ssfin4  8123  canthp1lem1  8460  nqereq  8745  ltexnq  8785  ltbtwnnq  8788  add20  9472  mullt0  9479  ltm1  9782  recgt0  9786  prodgt0  9787  prodge0  9789  ltmul1a  9791  recp1lt1  9840  recreclt  9841  ledivp1  9844  ledivp1i  9868  ltdivp1i  9869  ltaddrp2d  10610  xleadd1a  10764  xov1plusxeqvd  10973  fz01en  11011  fladdz  11154  flhalf  11158  fldiv  11168  modsubdir  11212  fzen2  11235  serle  11305  ltexp2a  11358  leexp2a  11362  exple1  11366  expubnd  11367  bernneq  11432  expmulnbnd  11438  discr1  11442  discr  11443  faclbnd6  11517  hashfz  11619  hashfun  11627  seqcoll  11639  sqeqd  11898  sqrlem7  11981  sqrge0  11990  sqrneglem  11999  abslt  12045  absle  12046  abstri  12061  rlimge0  12302  reccn2  12317  climaddc2  12356  isercolllem1  12385  caucvgrlem  12393  summolem2a  12436  isumge0  12477  fsumle  12505  fsumlt  12506  o1fsum  12519  supcvg  12562  expcnv  12570  geolim  12574  geolim2  12575  georeclim  12576  geo2lim  12579  mertenslem1  12588  mertens  12590  efcllem  12607  ef0lem  12608  efgt0  12631  eftlub  12637  eflt  12645  sinbnd  12708  cosbnd  12709  ef01bndlem  12712  sin01gt0  12718  cos01gt0  12719  sin02gt0  12720  eirrlem  12730  rpnnen2lem11  12751  rpnnen2  12752  ruclem11  12766  dvdssub2  12814  dvdsadd2b  12819  dvdsexp  12832  3dvds  12839  bitsfzolem  12873  bitsinv1lem  12880  bezoutlem4  12968  dvdsgcd  12970  dvdsmulgcd  12981  nn0seqcvgd  12988  prmind2  13017  rpmulgcd2  13032  qredeq  13033  rpdvds  13051  divdenle  13068  hashdvds  13091  phimullem  13095  eulerthlem2  13098  prmdiveq  13102  prmdivdiv  13103  opoe  13112  pythagtriplem4  13120  pythagtriplem10  13121  pythagtriplem19  13134  iserodd  13136  pcpre1  13143  pcadd2  13186  qexpz  13197  expnprm  13198  pockthlem  13200  prmreclem2  13212  prmreclem3  13213  4sqlem7  13239  4sqlem10  13242  4sqlem11  13250  4sqlem12  13251  4sqlem14  13253  4sqlem15  13254  4sqlem16  13255  0ram  13315  ffthiso  14053  latmlej12  14447  divsgrp  14922  pgpfi1  15156  sylow1lem4  15162  sylow1lem5  15163  odcau  15165  pgpfi  15166  pgpssslw  15175  sylow3lem4  15191  sylow3lem6  15193  efgsfo  15298  frgp0  15319  odadd1  15390  odadd2  15391  odadd  15392  gexexlem  15394  lt6abl  15431  dprd2dlem1  15526  dprd2d2  15529  ablfacrplem  15550  ablfacrp  15551  ablfacrp2  15552  ablfac1b  15555  ablfac1eu  15558  pgpfac1lem3a  15561  ablfaclem2  15571  dvdsrid  15683  dvdsrtr  15684  dvdsrneg  15686  unitmulcl  15696  unitgrp  15699  unitnegcl  15713  isdrng2  15772  subrguss  15810  subrgunit  15813  abvsubtri  15850  fidomndrnglem  16293  psrbaglesupp  16360  gzrngunit  16687  prmirredlem  16696  znidomb  16765  mettri2  18280  xmetsym  18286  xmettri  18289  prdsxmetlem  18306  xblss2  18332  blhalf  18334  xmsge0  18383  ngptgp  18548  nrginvrcnlem  18597  nmoeq0  18641  cnmet  18677  blcvx  18700  opnreen  18733  metdcnlem  18738  metdstri  18752  metdsle  18753  metnrmlem1  18760  metnrmlem3  18762  lebnumlem1  18857  pi1inv  18948  cphnmf  19029  ipge0  19032  ipcau2  19062  tchcphlem1  19063  minveclem2  19194  minveclem3  19197  ovolssnul  19250  ovolctb  19253  ovolunnul  19263  ovoliunlem1  19265  ovoliun2  19269  ovoliunnul  19270  ioombl1lem4  19322  uniioombllem3  19344  uniioombllem4  19345  uniioombllem5  19346  uniioombl  19348  volcn  19365  vitalilem2  19368  vitalilem5  19371  itg1lea  19471  mbfi1fseqlem6  19479  mbfi1flimlem  19481  itg2eqa  19504  itg2splitlem  19507  itg2split  19508  itg2monolem1  19509  itg2cnlem2  19521  iblabsr  19588  iblmulc2  19589  dveflem  19730  dvef  19731  dvferm2lem  19737  dvlip  19744  c1liplem1  19747  dveq0  19751  dvlt0  19756  dvivthlem1  19759  lhop1  19765  dvfsumle  19772  dvfsumlem4  19780  dvfsumrlim3  19784  dvfsum2  19785  ftc1a  19788  ftc1lem4  19790  deg1add  19893  ply1divex  19926  ply1rem  19953  fta1glem2  19956  fta1blem  19958  ig1pdvds  19966  plyeq0lem  19996  dgrcolem2  20059  plydivlem4  20080  plyrem  20089  fta1lem  20091  aalioulem3  20118  aaliou2b  20125  aaliou3lem3  20128  aaliou3lem8  20129  ulmcn  20182  ulmdvlem1  20183  itgulm  20191  pserulm  20205  pserdvlem2  20211  abelthlem2  20215  abelthlem5  20218  abelthlem6  20219  abelthlem7  20221  abelthlem8  20222  abelthlem9  20223  sinq12gt0  20282  sinq34lt0t  20284  cosq14gt0  20285  cosq14ge0  20286  efif1olem3  20313  argimgt0  20374  argimlt0  20375  logneg2  20377  logcnlem3  20402  logcnlem4  20403  logtayllem  20417  logtayl2  20420  cxpsqrlem  20460  cxpsqr  20461  cxpaddlelem  20502  abscxpbnd  20504  loglesqr  20509  ang180lem2  20519  atanlogaddlem  20620  atanlogsublem  20622  atantan  20630  atans2  20638  atantayl  20644  leibpi  20649  log2tlbnd  20652  birthdaylem2  20658  birthdaylem3  20659  cxp2limlem  20681  jensenlem2  20693  jensen  20694  logdiflbnd  20700  emcllem2  20702  emcllem4  20704  harmonicbnd4  20716  fsumharmonic  20717  wilthlem3  20720  basellem1  20730  basellem3  20732  basellem4  20733  fsumdvdsdiaglem  20835  dvdsppwf1o  20838  dvdsmulf1o  20846  chteq0  20860  chtub  20863  chpub  20871  logfacubnd  20872  logfaclbnd  20873  logexprlim  20876  perfectlem2  20881  dchrfi  20906  bclbnd  20931  bposlem1  20935  bposlem3  20937  bposlem4  20938  bposlem6  20940  lgslem1  20947  lgsqrlem2  20993  lgsqrlem4  20995  lgseisenlem2  21001  lgsquadlem1  21005  lgsquadlem2  21006  lgsquad2lem1  21009  2sqlem3  21017  2sqlem4  21018  2sqlem8  21023  2sqlem11  21026  chebbnd1lem2  21031  chebbnd1lem3  21032  chtppilimlem1  21034  chpchtlim  21040  vmadivsum  21043  vmadivsumb  21044  rpvmasumlem  21048  dchrisumlem2  21051  dchrmusum2  21055  dchrvmasumlem2  21059  dchrvmasumlem3  21060  dchrisum0flblem2  21070  dchrisum0fno1  21072  dchrisum0re  21074  dchrisum0lem1  21077  dchrisum0lem2a  21078  mudivsum  21091  mulogsumlem  21092  mulog2sumlem2  21096  vmalogdivsum2  21099  selberglem2  21107  selbergb  21110  selberg2b  21113  logdivbnd  21117  selberg3lem1  21118  selberg3lem2  21119  selberg4lem1  21121  pntrmax  21125  pntrlog2bndlem2  21139  pntrlog2bndlem3  21140  pntrlog2bndlem5  21142  pntrlog2bndlem6a  21143  pntrlog2bndlem6  21144  pntrlog2bnd  21145  pntpbnd1a  21146  pntpbnd1  21147  pntpbnd2  21148  pntibndlem1  21150  pntibndlem2  21152  pntlemb  21158  pntlemq  21162  pntlemr  21163  pntlemj  21164  pntlemk  21167  qabvle  21186  padicabvcxp  21193  ostth2lem2  21195  ostth2lem3  21196  ostth2lem4  21197  ostth3  21199  nvge0  22011  smcnlem  22041  nmoub3i  22122  nmoub2i  22123  nmlno0lem  22142  minvecolem2  22225  htthlem  22268  norm3dif2  22501  bcs2  22532  chscllem2  22988  eigposi  23187  nmopub2tALT  23260  nmfnleub2  23277  nmlnop0iALT  23346  riesz1  23416  cnlnadjlem2  23419  nmopcoadji  23452  leopsq  23480  leopmul  23485  leopnmid  23489  nmopleid  23490  opsqrlem6  23496  0leopj  23537  hstle1  23577  strlem3a  23603  mdslmd4i  23684  cvexchlem  23719  cdj1i  23784  le2halvesd  23958  xlt2addrd  23960  xrge0tsmsd  24052  ofldsqr  24066  ofld0le1  24068  sqsscirc1  24110  esumle  24245  esummono  24246  esumlef  24250  esumcst  24251  aean  24389  dya2ub  24414  dya2icoseg  24421  lgamgulmlem2  24593  lgamgulm2  24599  lgambdd  24600  lgamucov  24601  lgamcvglem  24603  lgamcvg2  24618  gamcvg  24619  subfacval3  24654  sconpht2  24704  sconpi1  24705  rescon  24712  snmlff  24795  sinccvglem  24888  mulge0b  24970  prodmolem2a  25039  faclimlem2  25121  colinearalglem4  25562  axpaschlem  25593  axcontlem7  25623  btwnouttr2  25670  ltflcei  25950  volsupnfl  25956  itg2addnclem  25957  itg2addnc  25959  iblmulc2nc  25970  bddiblnc  25975  ftc1cnnclem  25978  csbrn  26147  geomcau  26156  bfplem2  26223  rrncmslem  26232  rrnequiv  26235  irrapxlem1  26576  pell1qrgaplem  26627  pell1qrgap  26628  monotoddzzfi  26696  jm2.24nn  26715  congtr  26721  congmul  26723  congsub  26726  fzmaxdif  26737  acongeq  26739  bezoutr1  26742  jm2.20nn  26759  jm2.25  26761  mapfien2  26927  hbtlem4  26999  dgrsub2  27008  mpaaeu  27024  idomsubgmo  27183  dvconstbi  27220  mulltgt0  27361  fmul01  27378  fmul01lt1lem1  27382  fmul01lt1lem2  27383  climrec  27397  climexp  27399  climneg  27404  stoweidlem1  27418  stoweidlem11  27428  stoweidlem13  27430  stoweidlem26  27443  stoweidlem34  27451  stoweidlem38  27455  stoweidlem42  27459  stoweidlem51  27468  stoweidlem59  27476  stirlinglem5  27495  stirlinglem6  27496  stirlinglem7  27497  stirlinglem10  27500  stirlinglem11  27501  stirlinglem12  27502  stirlinglem13  27503  stirlinglem15  27505  lsatcvatlem  29164  islshpcv  29168  atlatmstc  29434  cvlsupr7  29463  cvrval3  29527  cvrval5  29529  cvrexchlem  29533  atcvrj1  29545  cvrat3  29556  cvrat4  29557  atbtwn  29560  1cvratex  29587  hlatexch4  29595  3atlem1  29597  3atlem2  29598  atcvrlln2  29633  atcvrlln  29634  lplnllnneN  29670  llncvrlpln2  29671  4atlem3b  29712  lplncvrlvol2  29729  dalemswapyz  29770  dalemswapyzps  29804  dalem25  29812  dalem39  29825  dalem58  29844  dalem59  29845  lneq2at  29892  lncvrat  29896  dalawlem2  29986  dalawlem3  29987  dalawlem4  29988  dalawlem6  29990  dalawlem9  29993  dalawlem11  29995  dalawlem12  29996  lhpocnle  30130  lhpmcvr3  30139  lhpmcvr5N  30141  lhpmcvr6N  30142  4atexlemunv  30180  4atexlemc  30183  4atexlemex2  30185  lautm  30208  cdlemc2  30306  cdleme5  30354  cdleme11j  30381  cdleme16b  30393  cdlemednpq  30413  cdleme19e  30421  cdleme20i  30431  cdleme22a  30454  cdleme22cN  30456  cdleme22d  30457  cdleme22e  30458  cdleme22eALTN  30459  cdleme22f  30460  cdleme23c  30465  cdleme30a  30492  cdleme35a  30562  cdleme35b  30564  cdleme42h  30596  cdlemeg46rgv  30642  cdlemg8b  30742  cdlemg12e  30761  cdlemg13a  30765  cdlemg17pq  30786  cdlemg18c  30794  cdlemg19  30798  cdlemg21  30800  cdlemg31d  30814  cdlemg33a  30820  tendoid  30887  cdlemk4  30948  cdlemki  30955  cdlemk10  30957  cdlemksv2  30961  cdlemk12  30964  cdlemk14  30968  cdlemk15  30969  cdlemk1u  30973  cdlemk5u  30975  cdlemk12u  30986  cdlemk45  31061  cdlemk48  31064  dia2dimlem1  31179  dia2dimlem2  31180  dia2dimlem3  31181  cdlemm10N  31233  cdlemn2  31310  dihjustlem  31331  dihglbcpreN  31415  dihmeetlem3N  31420
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
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 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-br 4154
  Copyright terms: Public domain W3C validator