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

Theorem breqtrd 4463
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 4451 . 2  |-  ( ph  ->  ( A R B  <-> 
A R C ) )
41, 3mpbid 210 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1398   class class class wbr 4439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-br 4440
This theorem is referenced by:  breqtrrd  4465  syl5breq  4474  domunsn  7660  mapdom2  7681  phplem4  7692  mapfien2  7860  wemaplem2  7964  infdifsn  8064  cantnff  8084  infxpenlem  8382  pwcda1  8565  pwcdadom  8587  infmap2  8589  ssfin4  8681  canthp1lem1  9019  nqereq  9302  ltexnq  9342  ltbtwnnq  9345  add20  10060  mullt0  10068  ltm1  10378  recgt0  10382  prodgt0  10383  prodge0  10385  ltmul1a  10387  mulge0b  10408  recp1lt1  10438  recreclt  10439  ledivp1  10442  ledivp1i  10466  ltdivp1i  10467  ltaddrp2d  11289  xleadd1a  11448  xov1plusxeqvd  11669  fz01en  11716  fzonmapblen  11845  fladdz  11940  flhalf  11944  fldiv  11969  modsubdir  12040  fzen2  12064  serle  12147  ltexp2a  12202  leexp2a  12206  exple1  12210  expubnd  12211  bernneq  12277  expmulnbnd  12283  discr1  12287  discr  12288  faclbnd6  12362  hashfz  12472  hashfun  12482  seqcoll  12499  sqeqd  13084  sqrlem7  13167  sqrtge0  13176  sqrtneglem  13185  abslt  13232  absle  13233  abstri  13248  rlimge0  13489  reccn2  13504  climaddc2  13543  isercolllem1  13572  caucvgrlem  13580  summolem2a  13622  isumge0  13666  fsumle  13698  fsumlt  13699  o1fsum  13712  supcvg  13752  expcnv  13760  geolim  13764  geolim2  13765  georeclim  13766  geo2lim  13769  mertenslem1  13778  mertens  13780  prodmolem2a  13826  efcllem  13898  ef0lem  13899  efgt0  13923  eftlub  13929  eflt  13937  sinbnd  14000  cosbnd  14001  ef01bndlem  14004  sin01gt0  14010  cos01gt0  14011  sin02gt0  14012  eirrlem  14022  rpnnen2lem11  14045  rpnnen2  14046  ruclem11  14060  dvdssub2  14110  dvdsadd2b  14115  dvdsexp  14129  3dvds  14137  bitsfzolem  14171  bitsinv1lem  14178  bezoutlem4  14266  dvdsgcd  14268  dvdsmulgcd  14279  nn0seqcvgd  14286  prmind2  14315  rpmulgcd2  14333  qredeq  14334  rpdvds  14352  divdenle  14369  hashdvds  14392  phimullem  14396  eulerthlem2  14399  prmdiveq  14403  prmdivdiv  14404  opoe  14422  pythagtriplem4  14430  pythagtriplem10  14431  pythagtriplem19  14444  iserodd  14446  pcpre1  14453  pcadd2  14496  qexpz  14507  expnprm  14508  pockthlem  14510  prmreclem2  14522  prmreclem3  14523  4sqlem7  14549  4sqlem10  14552  4sqlem11  14560  4sqlem12  14561  4sqlem14  14563  4sqlem15  14564  4sqlem16  14565  0ram  14625  ffthiso  15420  latmlej12  15923  qusgrp  16458  pgpfi1  16817  sylow1lem4  16823  sylow1lem5  16824  odcau  16826  pgpfi  16827  pgpssslw  16836  sylow3lem4  16852  sylow3lem6  16854  efgsfo  16959  frgp0  16980  odadd1  17056  odadd2  17057  odadd  17058  gexexlem  17060  lt6abl  17099  gsumzsubmcl  17130  pwsgsum  17207  dprd2dlem1  17288  dprd2d2  17291  ablfacrplem  17314  ablfacrp  17315  ablfacrp2  17316  ablfac1b  17319  ablfac1eu  17322  pgpfac1lem3a  17325  ablfaclem2  17335  dvdsrid  17498  dvdsrtr  17499  dvdsrneg  17501  unitmulcl  17511  unitgrp  17514  unitnegcl  17528  isdrng2  17604  subrguss  17642  subrgunit  17645  abvsubtri  17682  fidomndrnglem  18153  psrbaglesupp  18215  psrbaglesuppOLD  18216  gzrngunit  18681  prmirredlem  18708  znidomb  18776  frlmgsum  18976  invrvald  19348  psmetsym  20983  psmettri  20984  mettri2  21013  xmetsym  21019  xmettri  21023  prdsxmetlem  21040  xblss2ps  21073  xblss2  21074  blhalf  21077  xmsge0  21135  ngptgp  21319  nrginvrcnlem  21368  nmoeq0  21412  cnmet  21448  blcvx  21472  opnreen  21505  metdcnlem  21510  metdstri  21524  metdsle  21525  metnrmlem1  21532  metnrmlem3  21534  lebnumlem1  21630  pi1inv  21721  cphnmf  21811  ipge0  21814  ipcau2  21846  tchcphlem1  21847  csbren  21995  minveclem2  22010  minveclem3  22013  ovolssnul  22067  ovolctb  22070  ovolunnul  22080  ovoliunlem1  22082  ovoliun2  22086  ovoliunnul  22087  ioombl1lem4  22140  uniioombllem3  22163  uniioombllem4  22164  uniioombllem5  22165  uniioombl  22167  volcn  22184  vitalilem2  22187  vitalilem5  22190  itg1lea  22288  mbfi1fseqlem6  22296  mbfi1flimlem  22298  itg2eqa  22321  itg2splitlem  22324  itg2split  22325  itg2monolem1  22326  itg2cnlem2  22338  iblabsr  22405  iblmulc2  22406  dveflem  22549  dvef  22550  dvferm2lem  22556  dvlip  22563  c1liplem1  22566  dveq0  22570  dvlt0  22575  dvivthlem1  22578  lhop1  22584  dvfsumle  22591  dvfsumlem4  22599  dvfsumrlim3  22603  dvfsum2  22604  ftc1a  22607  ftc1lem4  22609  deg1add  22673  ply1divex  22706  ply1rem  22733  fta1glem2  22736  fta1blem  22738  ig1pdvds  22746  plyeq0lem  22776  dgrcolem2  22840  plydivlem4  22861  plyrem  22870  fta1lem  22872  aalioulem3  22899  aaliou2b  22906  aaliou3lem3  22909  aaliou3lem8  22910  ulmcn  22963  ulmdvlem1  22964  itgulm  22972  pserulm  22986  pserdvlem2  22992  abelthlem2  22996  abelthlem5  22999  abelthlem6  23000  abelthlem7  23002  abelthlem8  23003  abelthlem9  23004  sinq12gt0  23069  sinq34lt0t  23071  cosq14gt0  23072  cosq14ge0  23073  efif1olem3  23100  argimgt0  23168  argimlt0  23169  logneg2  23171  logcnlem3  23196  logcnlem4  23197  logtayllem  23211  logtayl2  23214  cxpsqrtlem  23254  cxpsqrt  23255  cxpaddlelem  23296  abscxpbnd  23298  loglesqrt  23303  ang180lem2  23344  atanlogaddlem  23444  atanlogsublem  23446  atantan  23454  atans2  23462  atantayl  23468  leibpi  23473  log2tlbnd  23476  birthdaylem2  23483  birthdaylem3  23484  cxp2limlem  23506  jensenlem2  23518  jensen  23519  logdiflbnd  23525  emcllem2  23527  emcllem4  23529  harmonicbnd4  23541  fsumharmonic  23542  wilthlem3  23545  basellem1  23555  basellem3  23557  basellem4  23558  fsumdvdsdiaglem  23660  dvdsppwf1o  23663  dvdsmulf1o  23671  chteq0  23685  chtub  23688  chpub  23696  logfacubnd  23697  logfaclbnd  23698  logexprlim  23701  perfectlem2  23706  dchrfi  23731  bclbnd  23756  bposlem1  23760  bposlem3  23762  bposlem4  23763  bposlem6  23765  lgslem1  23772  lgsqrlem2  23818  lgsqrlem4  23820  lgseisenlem2  23826  lgsquadlem1  23830  lgsquadlem2  23831  lgsquad2lem1  23834  2sqlem3  23842  2sqlem4  23843  2sqlem8  23848  2sqlem11  23851  chebbnd1lem2  23856  chebbnd1lem3  23857  chtppilimlem1  23859  chpchtlim  23865  vmadivsum  23868  vmadivsumb  23869  rpvmasumlem  23873  dchrisumlem2  23876  dchrmusum2  23880  dchrvmasumlem2  23884  dchrvmasumlem3  23885  dchrisum0flblem2  23895  dchrisum0fno1  23897  dchrisum0re  23899  dchrisum0lem1  23902  dchrisum0lem2a  23903  mudivsum  23916  mulogsumlem  23917  mulog2sumlem2  23921  vmalogdivsum2  23924  selberglem2  23932  selbergb  23935  selberg2b  23938  logdivbnd  23942  selberg3lem1  23943  selberg3lem2  23944  selberg4lem1  23946  pntrmax  23950  pntrlog2bndlem2  23964  pntrlog2bndlem3  23965  pntrlog2bndlem5  23967  pntrlog2bndlem6a  23968  pntrlog2bndlem6  23969  pntrlog2bnd  23970  pntpbnd1a  23971  pntpbnd1  23972  pntpbnd2  23973  pntibndlem1  23975  pntibndlem2  23977  pntlemb  23983  pntlemq  23987  pntlemr  23988  pntlemj  23989  pntlemk  23992  qabvle  24011  padicabvcxp  24018  ostth2lem2  24020  ostth2lem3  24021  ostth2lem4  24022  ostth3  24024  legtrid  24182  legov3  24188  krippenlem  24271  mideulem2  24312  midex  24315  opphllem5  24327  opphllem6  24328  opphl  24329  lmieu  24354  lmiisolem  24365  ttgcontlem1  24393  colinearalglem4  24417  axpaschlem  24448  axcontlem7  24478  clwlkndivn  25058  nvge0  25778  smcnlem  25808  nmoub3i  25889  nmoub2i  25890  nmlno0lem  25909  minvecolem2  25992  htthlem  26035  norm3dif2  26269  bcs2  26300  chscllem2  26757  eigposi  26956  nmopub2tALT  27029  nmfnleub2  27046  nmlnop0iALT  27115  riesz1  27185  cnlnadjlem2  27188  nmopcoadji  27221  leopsq  27249  leopmul  27254  leopnmid  27258  nmopleid  27259  opsqrlem6  27265  0leopj  27306  hstle1  27346  strlem3a  27372  mdslmd4i  27453  cvexchlem  27488  cdj1i  27553  mul2lt0bi  27803  le2halvesd  27810  xlt2addrd  27812  2sqcoprm  27872  2sqmod  27873  archiabllem1a  27972  archiabllem2a  27975  archiabllem2c  27976  xrge0tsmsd  28013  orngsqr  28032  ornglmulle  28033  orngrmulle  28034  orng0le1  28040  metideq  28110  metider  28111  sqsscirc1  28128  esummono  28286  esumpad2  28288  esumle  28290  esumlef  28294  esumcst  28295  esumrnmpt2  28300  esum2d  28325  aean  28456  dya2ub  28481  dya2icoseg  28488  omssubaddlem  28510  omssubadd  28511  inelcarsg  28522  carsgsigalem  28526  carsggect  28529  carsgclctunlem2  28530  eulerpartlemb  28574  fibp1  28607  sgnmulsgp  28756  eluzmn  28758  signsplypnf  28774  signsply0  28775  lgamgulmlem2  28839  lgamgulm2  28845  lgambdd  28846  lgamucov  28847  lgamcvglem  28849  lgamcvg2  28864  gamcvg  28865  subfacval3  28900  sconpht2  28950  sconpi1  28951  rescon  28958  snmlff  29041  sinccvglem  29305  faclimlem2  29413  btwnouttr2  29903  ltflcei  30286  heicant  30292  mblfinlem2  30295  mblfinlem3  30296  mblfinlem4  30297  volsupnfl  30302  dvtanlem  30307  itg2addnclem  30309  itg2addnclem3  30311  iblmulc2nc  30323  bddiblnc  30328  ftc1cnnclem  30331  ftc1anclem6  30338  ftc1anclem7  30339  ftc1anclem8  30340  ftc2nc  30342  dvasin  30346  geomcau  30495  bfplem2  30562  rrncmslem  30571  rrnequiv  30574  irrapxlem1  31000  pell1qrgaplem  31051  pell1qrgap  31052  monotoddzzfi  31120  jm2.24nn  31139  congtr  31145  congmul  31147  congsub  31150  fzmaxdif  31161  acongeq  31163  bezoutr1  31166  jm2.20nn  31181  jm2.25  31183  mapfien2OLD  31284  hbtlem4  31319  dgrsub2  31328  mpaaeu  31343  idomsubgmo  31399  cvgdvgrat  31438  radcnvrat  31439  hashnzfzclim  31471  dvconstbi  31483  binomcxplemdvbinom  31502  mulltgt0  31640  oddfl  31702  2timesgt  31718  lt3addmuld  31743  lt4addmuld  31748  iccshift  31800  iooshift  31804  fsumnncl  31814  fmul01  31816  fmul01lt1lem1  31820  fmul01lt1lem2  31821  mccllem  31847  climrec  31851  climexp  31853  climneg  31858  limcrecl  31877  sumnnodd  31878  lptioo2  31879  lptioo1  31880  ltmod  31886  lptre2pt  31888  0ellimcdiv  31897  limclner  31899  cncficcgt0  31933  cncfioobdlem  31941  ioodvbdlimc1lem1  31970  ioodvbdlimc1lem2  31971  ioodvbdlimc2lem  31973  dvdsn1add  31978  dvnxpaek  31981  dvnmul  31982  dvnprodlem1  31985  itgiccshift  32021  itgperiod  32022  stoweidlem1  32025  stoweidlem11  32035  stoweidlem13  32037  stoweidlem26  32050  stoweidlem34  32058  stoweidlem38  32062  stoweidlem42  32066  stoweidlem51  32075  stoweidlem59  32083  stirlinglem5  32102  stirlinglem6  32103  stirlinglem7  32104  stirlinglem10  32107  stirlinglem11  32108  stirlinglem13  32110  stirlinglem15  32112  dirkercncflem1  32127  dirkercncflem4  32130  fourierdlem4  32135  fourierdlem10  32141  fourierdlem11  32142  fourierdlem15  32146  fourierdlem20  32151  fourierdlem25  32156  fourierdlem26  32157  fourierdlem30  32161  fourierdlem37  32168  fourierdlem39  32170  fourierdlem40  32171  fourierdlem41  32172  fourierdlem42  32173  fourierdlem44  32175  fourierdlem47  32178  fourierdlem48  32179  fourierdlem49  32180  fourierdlem50  32181  fourierdlem51  32182  fourierdlem52  32183  fourierdlem54  32185  fourierdlem60  32191  fourierdlem61  32192  fourierdlem63  32194  fourierdlem64  32195  fourierdlem65  32196  fourierdlem73  32204  fourierdlem74  32205  fourierdlem75  32206  fourierdlem76  32207  fourierdlem78  32209  fourierdlem79  32210  fourierdlem81  32212  fourierdlem84  32215  fourierdlem87  32218  fourierdlem92  32223  fourierdlem93  32224  fourierdlem101  32232  fourierdlem102  32233  fourierdlem103  32234  fourierdlem104  32235  fourierdlem111  32242  fourierdlem114  32245  sqwvfoura  32253  sqwvfourb  32254  fouriersw  32256  etransclem19  32278  etransclem23  32282  etransclem24  32283  etransclem25  32284  etransclem27  32286  etransclem32  32291  etransclem35  32294  etransclem48  32307  perfectALTVlem2  32616  nnpw2blen  33474  isosctrlem1ALT  34154  lsatcvatlem  35190  islshpcv  35194  atlatmstc  35460  cvlsupr7  35489  cvrval3  35553  cvrval5  35555  cvrexchlem  35559  atcvrj1  35571  cvrat3  35582  cvrat4  35583  atbtwn  35586  1cvratex  35613  hlatexch4  35621  3atlem1  35623  3atlem2  35624  atcvrlln2  35659  atcvrlln  35660  lplnllnneN  35696  llncvrlpln2  35697  4atlem3b  35738  lplncvrlvol2  35755  dalemswapyz  35796  dalemswapyzps  35830  dalem25  35838  dalem39  35851  dalem58  35870  dalem59  35871  lneq2at  35918  lncvrat  35922  dalawlem2  36012  dalawlem3  36013  dalawlem4  36014  dalawlem6  36016  dalawlem9  36019  dalawlem11  36021  dalawlem12  36022  lhpocnle  36156  lhpmcvr3  36165  lhpmcvr5N  36167  lhpmcvr6N  36168  4atexlemunv  36206  4atexlemc  36209  4atexlemex2  36211  lautm  36234  cdlemc2  36333  cdleme5  36381  cdleme11j  36408  cdleme16b  36420  cdlemednpq  36440  cdleme19e  36449  cdleme20i  36459  cdleme22a  36482  cdleme22cN  36484  cdleme22d  36485  cdleme22e  36486  cdleme22eALTN  36487  cdleme22f  36488  cdleme23c  36493  cdleme30a  36520  cdleme35a  36590  cdleme35b  36592  cdleme42h  36624  cdlemeg46rgv  36670  cdlemg8b  36770  cdlemg12e  36789  cdlemg13a  36793  cdlemg17pq  36814  cdlemg18c  36822  cdlemg19  36826  cdlemg21  36828  cdlemg31d  36842  cdlemg33a  36848  tendoid  36915  cdlemk4  36976  cdlemki  36983  cdlemk10  36985  cdlemksv2  36989  cdlemk12  36992  cdlemk14  36996  cdlemk15  36997  cdlemk1u  37001  cdlemk5u  37003  cdlemk12u  37014  cdlemk45  37089  cdlemk48  37092  dia2dimlem1  37207  dia2dimlem2  37208  dia2dimlem3  37209  cdlemm10N  37261  cdlemn2  37338  dihjustlem  37359  dihglbcpreN  37443  dihmeetlem3N  37448  int-sqgeq0d  38520  int-ineqmvtd  38525
  Copyright terms: Public domain W3C validator