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

Theorem breqtrd 4450
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 4438 . 2  |-  ( ph  ->  ( A R B  <-> 
A R C ) )
41, 3mpbid 213 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437   class class class wbr 4426
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-br 4427
This theorem is referenced by:  breqtrrd  4452  syl5breq  4461  domunsn  7728  mapdom2  7749  phplem4  7760  mapfien2  7928  wemaplem2  8062  infdifsn  8161  cantnff  8178  infxpenlem  8443  pwcda1  8622  pwcdadom  8644  infmap2  8646  ssfin4  8738  canthp1lem1  9076  nqereq  9359  ltexnq  9399  ltbtwnnq  9402  add20  10125  mullt0  10132  ltm1  10444  recgt0  10448  prodgt0  10449  prodge0  10451  ltmul1a  10453  mulge0b  10474  recp1lt1  10504  recreclt  10505  ledivp1  10508  ledivp1i  10532  ltdivp1i  10533  ltaddrp2d  11372  mul2lt0bi  11402  xleadd1a  11539  xov1plusxeqvd  11776  fz01en  11825  fzonmapblen  11959  fladdz  12055  flhalf  12059  fldiv  12084  modsubdir  12155  fzen2  12179  serle  12265  ltexp2a  12321  leexp2a  12325  exple1  12329  expubnd  12330  bernneq  12395  expmulnbnd  12401  discr1  12405  discr  12406  faclbnd6  12481  hashfz  12594  hashfun  12604  seqcoll  12621  sqeqd  13208  sqrlem7  13291  sqrtge0  13300  sqrtneglem  13309  abslt  13356  absle  13357  abstri  13372  rlimge0  13623  reccn2  13638  climaddc2  13677  isercolllem1  13706  caucvgrlem  13714  caucvgrlemOLD  13715  summolem2a  13759  isumge0  13805  fsumle  13837  fsumlt  13838  o1fsum  13851  supcvg  13892  expcnv  13900  geolim  13904  geolim2  13905  georeclim  13906  geo2lim  13909  mertenslem1  13918  mertens  13920  prodmolem2a  13966  efcllem  14110  ef0lem  14111  efgt0  14135  eftlub  14141  eflt  14149  sinbnd  14212  cosbnd  14213  ef01bndlem  14216  sin01gt0  14222  cos01gt0  14223  sin02gt0  14224  eirrlem  14234  rpnnen2lem11  14255  rpnnen2  14256  ruclem11  14270  dvdssub2  14320  dvdsadd2b  14325  dvdsexp  14339  3dvds  14347  bitsfzolem  14382  bitsinv1lem  14389  bezoutlem4  14480  dvdsgcd  14482  dvdsmulgcd  14493  nn0seqcvgd  14500  prmind2  14606  rpmulgcd2  14633  qredeq  14634  rpdvds  14647  divdenle  14669  hashdvds  14692  phimullem  14696  eulerthlem2  14699  prmdiveq  14703  prmdivdiv  14704  opoe  14724  pythagtriplem4  14732  pythagtriplem10  14733  pythagtriplem19  14746  iserodd  14748  pcpre1  14755  pcadd2  14798  qexpz  14809  expnprm  14810  pockthlem  14812  prmreclem2  14824  prmreclem3  14825  4sqlem7  14851  4sqlem10  14854  4sqlem11  14862  4sqlem12  14863  4sqlem14OLD  14865  4sqlem15OLD  14866  4sqlem16OLD  14867  4sqlem14  14871  4sqlem15  14872  4sqlem16  14873  0ram  14941  ffthiso  15785  latmlej12  16288  qusgrp  16823  pgpfi1  17182  sylow1lem4  17188  sylow1lem5  17189  odcau  17191  pgpfi  17192  pgpssslw  17201  sylow3lem4  17217  sylow3lem6  17219  efgsfo  17324  frgp0  17345  odadd1  17421  odadd2  17422  odadd  17423  gexexlem  17425  lt6abl  17464  gsumzsubmcl  17486  pwsgsum  17546  dprd2dlem1  17609  dprd2d2  17612  ablfacrplem  17633  ablfacrp  17634  ablfacrp2  17635  ablfac1b  17638  ablfac1eu  17641  pgpfac1lem3a  17644  ablfaclem2  17654  dvdsrid  17814  dvdsrtr  17815  dvdsrneg  17817  unitmulcl  17827  unitgrp  17830  unitnegcl  17844  isdrng2  17920  subrguss  17958  subrgunit  17961  abvsubtri  17998  fidomndrnglem  18465  psrbaglesupp  18527  gzrngunit  18968  prmirredlem  18995  znidomb  19063  frlmgsum  19261  invrvald  19632  psmetsym  21257  psmettri  21258  mettri2  21287  xmetsym  21293  xmettri  21297  prdsxmetlem  21314  xblss2ps  21347  xblss2  21348  blhalf  21351  xmsge0  21409  ngptgp  21575  nrginvrcnlem  21624  nmoeq0  21668  cnmet  21703  blcvx  21727  opnreen  21760  metdcnlem  21765  metdstri  21779  metdsle  21780  metnrmlem1  21787  metnrmlem3  21789  lebnumlem1  21885  pi1inv  21976  cphnmf  22066  ipge0  22069  ipcau2  22101  tchcphlem1  22102  csbren  22246  minveclem2  22261  minveclem3  22264  ovolssnul  22318  ovolctb  22321  ovolunnul  22331  ovoliunlem1  22333  ovoliun2  22337  ovoliunnul  22338  ioombl1lem4  22391  uniioombllem3  22420  uniioombllem4  22421  uniioombllem5  22422  uniioombl  22424  volcn  22441  vitalilem2  22444  vitalilem5  22447  itg1lea  22547  mbfi1fseqlem6  22555  mbfi1flimlem  22557  itg2eqa  22580  itg2splitlem  22583  itg2split  22584  itg2monolem1  22585  itg2cnlem2  22597  iblabsr  22664  iblmulc2  22665  dveflem  22808  dvef  22809  dvferm2lem  22815  dvlip  22822  c1liplem1  22825  dveq0  22829  dvlt0  22834  dvivthlem1  22837  lhop1  22843  dvfsumle  22850  dvfsumlem4  22858  dvfsumrlim3  22862  dvfsum2  22863  ftc1a  22866  ftc1lem4  22868  deg1add  22929  ply1divex  22962  ply1rem  22989  fta1glem2  22992  fta1blem  22994  ig1pdvds  23002  plyeq0lem  23032  dgrcolem2  23096  plydivlem4  23117  plyrem  23126  fta1lem  23128  aalioulem3  23155  aaliou2b  23162  aaliou3lem3  23165  aaliou3lem8  23166  ulmcn  23219  ulmdvlem1  23220  itgulm  23228  pserulm  23242  pserdvlem2  23248  abelthlem2  23252  abelthlem5  23255  abelthlem6  23256  abelthlem7  23258  abelthlem8  23259  abelthlem9  23260  sinq12gt0  23327  sinq34lt0t  23329  cosq14gt0  23330  cosq14ge0  23331  efif1olem3  23358  argimgt0  23426  argimlt0  23427  logneg2  23429  logcnlem3  23454  logcnlem4  23455  logtayllem  23469  logtayl2  23472  cxpsqrtlem  23512  cxpsqrt  23513  cxpaddlelem  23556  abscxpbnd  23558  loglesqrt  23563  ang180lem2  23604  atanlogaddlem  23704  atanlogsublem  23706  atantan  23714  atans2  23722  atantayl  23728  leibpi  23733  log2tlbnd  23736  birthdaylem2  23743  birthdaylem3  23744  cxp2limlem  23766  jensenlem2  23778  jensen  23779  logdiflbnd  23785  emcllem2  23787  emcllem4  23789  harmonicbnd4  23801  fsumharmonic  23802  lgamgulmlem2  23820  lgamgulm2  23826  lgambdd  23827  lgamucov  23828  lgamcvglem  23830  lgamcvg2  23845  gamcvg  23846  wilthlem3  23860  basellem1  23870  basellem3  23872  basellem4  23873  fsumdvdsdiaglem  23975  dvdsppwf1o  23978  dvdsmulf1o  23986  chteq0  24000  chtub  24003  chpub  24011  logfacubnd  24012  logfaclbnd  24013  logexprlim  24016  perfectlem2  24021  dchrfi  24046  bclbnd  24071  bposlem1  24075  bposlem3  24077  bposlem4  24078  bposlem6  24080  lgslem1  24087  lgsqrlem2  24133  lgsqrlem4  24135  lgseisenlem2  24141  lgsquadlem1  24145  lgsquadlem2  24146  lgsquad2lem1  24149  2sqlem3  24157  2sqlem4  24158  2sqlem8  24163  2sqlem11  24166  chebbnd1lem2  24171  chebbnd1lem3  24172  chtppilimlem1  24174  chpchtlim  24180  vmadivsum  24183  vmadivsumb  24184  rpvmasumlem  24188  dchrisumlem2  24191  dchrmusum2  24195  dchrvmasumlem2  24199  dchrvmasumlem3  24200  dchrisum0flblem2  24210  dchrisum0fno1  24212  dchrisum0re  24214  dchrisum0lem1  24217  dchrisum0lem2a  24218  mudivsum  24231  mulogsumlem  24232  mulog2sumlem2  24236  vmalogdivsum2  24239  selberglem2  24247  selbergb  24250  selberg2b  24253  logdivbnd  24257  selberg3lem1  24258  selberg3lem2  24259  selberg4lem1  24261  pntrmax  24265  pntrlog2bndlem2  24279  pntrlog2bndlem3  24280  pntrlog2bndlem5  24282  pntrlog2bndlem6a  24283  pntrlog2bndlem6  24284  pntrlog2bnd  24285  pntpbnd1a  24286  pntpbnd1  24287  pntpbnd2  24288  pntibndlem1  24290  pntibndlem2  24292  pntlemb  24298  pntlemq  24302  pntlemr  24303  pntlemj  24304  pntlemk  24307  qabvle  24326  padicabvcxp  24333  ostth2lem2  24335  ostth2lem3  24336  ostth2lem4  24337  ostth3  24339  legtrid  24496  legov3  24503  krippenlem  24592  mideulem2  24633  midex  24636  opphllem5  24650  opphllem6  24651  opphl  24653  lmieu  24682  lmiisolem  24694  ttgcontlem1  24761  colinearalglem4  24785  axpaschlem  24816  axcontlem7  24846  clwlkndivn  25426  nvge0  26148  smcnlem  26178  nmoub3i  26259  nmoub2i  26260  nmlno0lem  26279  minvecolem2  26362  htthlem  26405  norm3dif2  26639  bcs2  26670  chscllem2  27126  eigposi  27324  nmopub2tALT  27397  nmfnleub2  27414  nmlnop0iALT  27483  riesz1  27553  cnlnadjlem2  27556  nmopcoadji  27589  leopsq  27617  leopmul  27622  leopnmid  27626  nmopleid  27627  opsqrlem6  27633  0leopj  27674  hstle1  27714  strlem3a  27740  mdslmd4i  27821  cvexchlem  27856  cdj1i  27921  le2halvesd  28176  xlt2addrd  28179  2sqcoprm  28246  2sqmod  28247  archiabllem1a  28346  archiabllem2a  28349  archiabllem2c  28350  xrge0tsmsd  28387  orngsqr  28406  ornglmulle  28407  orngrmulle  28408  orng0le1  28414  fzto1st1  28454  metideq  28535  metider  28536  sqsscirc1  28553  esummono  28714  esumpad2  28716  esumle  28718  esumlef  28722  esumcst  28723  esumrnmpt2  28728  esum2d  28753  aean  28906  dya2ub  28931  dya2icoseg  28938  omssubaddlem  28960  omssubadd  28961  inelcarsg  28972  carsgsigalem  28976  carsggect  28979  carsgclctunlem2  28980  eulerpartlemb  29027  fibp1  29060  sgnmulsgp  29209  eluzmn  29211  signsplypnf  29227  signsply0  29228  subfacval3  29700  sconpht2  29749  sconpi1  29750  rescon  29757  snmlff  29840  sinccvglem  30104  faclimlem2  30167  btwnouttr2  30574  ltflcei  31636  poimirlem9  31652  poimirlem26  31669  poimirlem27  31670  poimirlem29  31672  heicant  31678  mblfinlem2  31681  mblfinlem3  31682  mblfinlem4  31683  volsupnfl  31688  dvtanlemOLD  31694  itg2addnclem  31696  itg2addnclem3  31698  iblmulc2nc  31710  bddiblnc  31715  ftc1cnnclem  31718  ftc1anclem6  31725  ftc1anclem7  31726  ftc1anclem8  31727  ftc2nc  31729  dvasin  31731  geomcau  31791  bfplem2  31858  rrncmslem  31867  rrnequiv  31870  lsatcvatlem  32323  islshpcv  32327  atlatmstc  32593  cvlsupr7  32622  cvrval3  32686  cvrval5  32688  cvrexchlem  32692  atcvrj1  32704  cvrat3  32715  cvrat4  32716  atbtwn  32719  1cvratex  32746  hlatexch4  32754  3atlem1  32756  3atlem2  32757  atcvrlln2  32792  atcvrlln  32793  lplnllnneN  32829  llncvrlpln2  32830  4atlem3b  32871  lplncvrlvol2  32888  dalemswapyz  32929  dalemswapyzps  32963  dalem25  32971  dalem39  32984  dalem58  33003  dalem59  33004  lneq2at  33051  lncvrat  33055  dalawlem2  33145  dalawlem3  33146  dalawlem4  33147  dalawlem6  33149  dalawlem9  33152  dalawlem11  33154  dalawlem12  33155  lhpocnle  33289  lhpmcvr3  33298  lhpmcvr5N  33300  lhpmcvr6N  33301  4atexlemunv  33339  4atexlemc  33342  4atexlemex2  33344  lautm  33367  cdlemc2  33466  cdleme5  33514  cdleme11j  33541  cdleme16b  33553  cdlemednpq  33573  cdleme19e  33582  cdleme20i  33592  cdleme22a  33615  cdleme22cN  33617  cdleme22d  33618  cdleme22e  33619  cdleme22eALTN  33620  cdleme22f  33621  cdleme23c  33626  cdleme30a  33653  cdleme35a  33723  cdleme35b  33725  cdleme42h  33757  cdlemeg46rgv  33803  cdlemg8b  33903  cdlemg12e  33922  cdlemg13a  33926  cdlemg17pq  33947  cdlemg18c  33955  cdlemg19  33959  cdlemg21  33961  cdlemg31d  33975  cdlemg33a  33981  tendoid  34048  cdlemk4  34109  cdlemki  34116  cdlemk10  34118  cdlemksv2  34122  cdlemk12  34125  cdlemk14  34129  cdlemk15  34130  cdlemk1u  34134  cdlemk5u  34136  cdlemk12u  34147  cdlemk45  34222  cdlemk48  34225  dia2dimlem1  34340  dia2dimlem2  34341  dia2dimlem3  34342  cdlemm10N  34394  cdlemn2  34471  dihjustlem  34492  dihglbcpreN  34576  dihmeetlem3N  34581  irrapxlem1  35375  pell1qrgaplem  35426  pell1qrgap  35427  monotoddzzfi  35495  jm2.24nn  35514  congtr  35520  congmul  35522  congsub  35525  fzmaxdif  35536  acongeq  35538  bezoutr1  35541  jm2.20nn  35557  jm2.25  35559  hbtlem4  35690  dgrsub2  35699  mpaaeu  35714  idomsubgmo  35770  int-sqgeq0d  36269  int-ineqmvtd  36274  cvgdvgrat  36298  radcnvrat  36299  hashnzfzclim  36307  dvconstbi  36319  binomcxplemdvbinom  36338  isosctrlem1ALT  36970  mulltgt0  36982  oddfl  37095  2timesgt  37109  lt3addmuld  37127  lt4addmuld  37132  supxrgere  37164  supxrgelem  37168  supxrge  37169  iccshift  37203  iooshift  37207  fsumnncl  37224  fmul01  37229  fmul01lt1lem1  37233  fmul01lt1lem2  37234  mccllem  37248  climrec  37252  climexp  37254  climneg  37260  limcrecl  37280  sumnnodd  37281  lptioo2  37282  lptioo1  37283  ltmod  37289  lptre2pt  37291  0ellimcdiv  37301  limclner  37303  cncficcgt0  37337  cncfioobdlem  37345  ioodvbdlimc1lem1  37374  ioodvbdlimc1lem2  37375  ioodvbdlimc2lem  37377  dvdsn1add  37382  dvnxpaek  37385  dvnmul  37386  dvnprodlem1  37389  itgiccshift  37425  itgperiod  37426  stoweidlem1  37429  stoweidlem11  37439  stoweidlem13  37441  stoweidlem26  37454  stoweidlem34  37463  stoweidlem38  37467  stoweidlem42  37471  stoweidlem51  37480  stoweidlem59  37488  stirlinglem5  37508  stirlinglem6  37509  stirlinglem7  37510  stirlinglem10  37513  stirlinglem11  37514  stirlinglem13  37516  stirlinglem15  37518  dirkercncflem1  37533  dirkercncflem4  37536  fourierdlem4  37541  fourierdlem10  37547  fourierdlem11  37548  fourierdlem15  37552  fourierdlem20  37557  fourierdlem25  37562  fourierdlem26  37563  fourierdlem30  37567  fourierdlem37  37574  fourierdlem39  37576  fourierdlem40  37577  fourierdlem41  37578  fourierdlem42  37579  fourierdlem44  37581  fourierdlem47  37584  fourierdlem48  37585  fourierdlem49  37586  fourierdlem50  37587  fourierdlem51  37588  fourierdlem52  37589  fourierdlem54  37591  fourierdlem60  37597  fourierdlem61  37598  fourierdlem63  37600  fourierdlem64  37601  fourierdlem65  37602  fourierdlem73  37610  fourierdlem74  37611  fourierdlem75  37612  fourierdlem76  37613  fourierdlem78  37615  fourierdlem79  37616  fourierdlem81  37618  fourierdlem84  37621  fourierdlem87  37624  fourierdlem92  37629  fourierdlem93  37630  fourierdlem101  37638  fourierdlem102  37639  fourierdlem103  37640  fourierdlem104  37641  fourierdlem111  37648  fourierdlem114  37651  sqwvfoura  37659  sqwvfourb  37660  fouriersw  37662  etransclem19  37684  etransclem23  37688  etransclem24  37689  etransclem25  37690  etransclem27  37692  etransclem32  37697  etransclem35  37700  etransclem48  37713  fsumlesge0  37752  sge0cl  37756  sge0supre  37764  sge0less  37767  sge0gerp  37770  sge0ltfirp  37775  sge0le  37782  sge0ltfirpmpt  37783  sge0split  37784  nnfoctbdjlem  37801  meassle  37809  omeiunle  37846  omeiunltfirp  37848  carageniuncllem2  37851  carageniuncl  37852  perfectALTVlem2  38233  nnpw2blen  39151
  Copyright terms: Public domain W3C validator