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

Theorem breqtrd 4204
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 4192 . 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 4180
This theorem is referenced by:  breqtrrd  4206  syl5breq  4215  domunsn  7224  mapdom2  7245  phplem4  7256  wemaplem2  7480  infdifsn  7575  cantnff  7593  infxpenlem  7859  pwcda1  8038  pwcdadom  8060  infmap2  8062  ssfin4  8154  canthp1lem1  8491  nqereq  8776  ltexnq  8816  ltbtwnnq  8819  add20  9504  mullt0  9511  ltm1  9814  recgt0  9818  prodgt0  9819  prodge0  9821  ltmul1a  9823  recp1lt1  9872  recreclt  9873  ledivp1  9876  ledivp1i  9900  ltdivp1i  9901  ltaddrp2d  10642  xleadd1a  10796  xov1plusxeqvd  11005  fz01en  11043  fladdz  11190  flhalf  11194  fldiv  11204  modsubdir  11248  fzen2  11271  serle  11341  ltexp2a  11394  leexp2a  11398  exple1  11402  expubnd  11403  bernneq  11468  expmulnbnd  11474  discr1  11478  discr  11479  faclbnd6  11553  hashfz  11655  hashfun  11663  seqcoll  11675  sqeqd  11934  sqrlem7  12017  sqrge0  12026  sqrneglem  12035  abslt  12081  absle  12082  abstri  12097  rlimge0  12338  reccn2  12353  climaddc2  12392  isercolllem1  12421  caucvgrlem  12429  summolem2a  12472  isumge0  12513  fsumle  12541  fsumlt  12542  o1fsum  12555  supcvg  12598  expcnv  12606  geolim  12610  geolim2  12611  georeclim  12612  geo2lim  12615  mertenslem1  12624  mertens  12626  efcllem  12643  ef0lem  12644  efgt0  12667  eftlub  12673  eflt  12681  sinbnd  12744  cosbnd  12745  ef01bndlem  12748  sin01gt0  12754  cos01gt0  12755  sin02gt0  12756  eirrlem  12766  rpnnen2lem11  12787  rpnnen2  12788  ruclem11  12802  dvdssub2  12850  dvdsadd2b  12855  dvdsexp  12868  3dvds  12875  bitsfzolem  12909  bitsinv1lem  12916  bezoutlem4  13004  dvdsgcd  13006  dvdsmulgcd  13017  nn0seqcvgd  13024  prmind2  13053  rpmulgcd2  13068  qredeq  13069  rpdvds  13087  divdenle  13104  hashdvds  13127  phimullem  13131  eulerthlem2  13134  prmdiveq  13138  prmdivdiv  13139  opoe  13148  pythagtriplem4  13156  pythagtriplem10  13157  pythagtriplem19  13170  iserodd  13172  pcpre1  13179  pcadd2  13222  qexpz  13233  expnprm  13234  pockthlem  13236  prmreclem2  13248  prmreclem3  13249  4sqlem7  13275  4sqlem10  13278  4sqlem11  13286  4sqlem12  13287  4sqlem14  13289  4sqlem15  13290  4sqlem16  13291  0ram  13351  ffthiso  14089  latmlej12  14483  divsgrp  14958  pgpfi1  15192  sylow1lem4  15198  sylow1lem5  15199  odcau  15201  pgpfi  15202  pgpssslw  15211  sylow3lem4  15227  sylow3lem6  15229  efgsfo  15334  frgp0  15355  odadd1  15426  odadd2  15427  odadd  15428  gexexlem  15430  lt6abl  15467  dprd2dlem1  15562  dprd2d2  15565  ablfacrplem  15586  ablfacrp  15587  ablfacrp2  15588  ablfac1b  15591  ablfac1eu  15594  pgpfac1lem3a  15597  ablfaclem2  15607  dvdsrid  15719  dvdsrtr  15720  dvdsrneg  15722  unitmulcl  15732  unitgrp  15735  unitnegcl  15749  isdrng2  15808  subrguss  15846  subrgunit  15849  abvsubtri  15886  fidomndrnglem  16329  psrbaglesupp  16396  gzrngunit  16727  prmirredlem  16736  znidomb  16805  psmetsym  18302  psmettri  18303  mettri2  18332  xmetsym  18338  xmettri  18342  prdsxmetlem  18359  xblss2ps  18392  xblss2  18393  blhalf  18396  xmsge0  18454  ngptgp  18638  nrginvrcnlem  18687  nmoeq0  18731  cnmet  18767  blcvx  18790  opnreen  18823  metdcnlem  18828  metdstri  18842  metdsle  18843  metnrmlem1  18850  metnrmlem3  18852  lebnumlem1  18947  pi1inv  19038  cphnmf  19119  ipge0  19122  ipcau2  19152  tchcphlem1  19153  minveclem2  19288  minveclem3  19291  ovolssnul  19344  ovolctb  19347  ovolunnul  19357  ovoliunlem1  19359  ovoliun2  19363  ovoliunnul  19364  ioombl1lem4  19416  uniioombllem3  19438  uniioombllem4  19439  uniioombllem5  19440  uniioombl  19442  volcn  19459  vitalilem2  19462  vitalilem5  19465  itg1lea  19565  mbfi1fseqlem6  19573  mbfi1flimlem  19575  itg2eqa  19598  itg2splitlem  19601  itg2split  19602  itg2monolem1  19603  itg2cnlem2  19615  iblabsr  19682  iblmulc2  19683  dveflem  19824  dvef  19825  dvferm2lem  19831  dvlip  19838  c1liplem1  19841  dveq0  19845  dvlt0  19850  dvivthlem1  19853  lhop1  19859  dvfsumle  19866  dvfsumlem4  19874  dvfsumrlim3  19878  dvfsum2  19879  ftc1a  19882  ftc1lem4  19884  deg1add  19987  ply1divex  20020  ply1rem  20047  fta1glem2  20050  fta1blem  20052  ig1pdvds  20060  plyeq0lem  20090  dgrcolem2  20153  plydivlem4  20174  plyrem  20183  fta1lem  20185  aalioulem3  20212  aaliou2b  20219  aaliou3lem3  20222  aaliou3lem8  20223  ulmcn  20276  ulmdvlem1  20277  itgulm  20285  pserulm  20299  pserdvlem2  20305  abelthlem2  20309  abelthlem5  20312  abelthlem6  20313  abelthlem7  20315  abelthlem8  20316  abelthlem9  20317  sinq12gt0  20376  sinq34lt0t  20378  cosq14gt0  20379  cosq14ge0  20380  efif1olem3  20407  argimgt0  20468  argimlt0  20469  logneg2  20471  logcnlem3  20496  logcnlem4  20497  logtayllem  20511  logtayl2  20514  cxpsqrlem  20554  cxpsqr  20555  cxpaddlelem  20596  abscxpbnd  20598  loglesqr  20603  ang180lem2  20613  atanlogaddlem  20714  atanlogsublem  20716  atantan  20724  atans2  20732  atantayl  20738  leibpi  20743  log2tlbnd  20746  birthdaylem2  20752  birthdaylem3  20753  cxp2limlem  20775  jensenlem2  20787  jensen  20788  logdiflbnd  20794  emcllem2  20796  emcllem4  20798  harmonicbnd4  20810  fsumharmonic  20811  wilthlem3  20814  basellem1  20824  basellem3  20826  basellem4  20827  fsumdvdsdiaglem  20929  dvdsppwf1o  20932  dvdsmulf1o  20940  chteq0  20954  chtub  20957  chpub  20965  logfacubnd  20966  logfaclbnd  20967  logexprlim  20970  perfectlem2  20975  dchrfi  21000  bclbnd  21025  bposlem1  21029  bposlem3  21031  bposlem4  21032  bposlem6  21034  lgslem1  21041  lgsqrlem2  21087  lgsqrlem4  21089  lgseisenlem2  21095  lgsquadlem1  21099  lgsquadlem2  21100  lgsquad2lem1  21103  2sqlem3  21111  2sqlem4  21112  2sqlem8  21117  2sqlem11  21120  chebbnd1lem2  21125  chebbnd1lem3  21126  chtppilimlem1  21128  chpchtlim  21134  vmadivsum  21137  vmadivsumb  21138  rpvmasumlem  21142  dchrisumlem2  21145  dchrmusum2  21149  dchrvmasumlem2  21153  dchrvmasumlem3  21154  dchrisum0flblem2  21164  dchrisum0fno1  21166  dchrisum0re  21168  dchrisum0lem1  21171  dchrisum0lem2a  21172  mudivsum  21185  mulogsumlem  21186  mulog2sumlem2  21190  vmalogdivsum2  21193  selberglem2  21201  selbergb  21204  selberg2b  21207  logdivbnd  21211  selberg3lem1  21212  selberg3lem2  21213  selberg4lem1  21215  pntrmax  21219  pntrlog2bndlem2  21233  pntrlog2bndlem3  21234  pntrlog2bndlem5  21236  pntrlog2bndlem6a  21237  pntrlog2bndlem6  21238  pntrlog2bnd  21239  pntpbnd1a  21240  pntpbnd1  21241  pntpbnd2  21242  pntibndlem1  21244  pntibndlem2  21246  pntlemb  21252  pntlemq  21256  pntlemr  21257  pntlemj  21258  pntlemk  21261  qabvle  21280  padicabvcxp  21287  ostth2lem2  21289  ostth2lem3  21290  ostth2lem4  21291  ostth3  21293  nvge0  22124  smcnlem  22154  nmoub3i  22235  nmoub2i  22236  nmlno0lem  22255  minvecolem2  22338  htthlem  22381  norm3dif2  22614  bcs2  22645  chscllem2  23101  eigposi  23300  nmopub2tALT  23373  nmfnleub2  23390  nmlnop0iALT  23459  riesz1  23529  cnlnadjlem2  23532  nmopcoadji  23565  leopsq  23593  leopmul  23598  leopnmid  23602  nmopleid  23603  opsqrlem6  23609  0leopj  23650  hstle1  23690  strlem3a  23716  mdslmd4i  23797  cvexchlem  23832  cdj1i  23897  le2halvesd  24083  xlt2addrd  24085  xrge0tsmsd  24184  ofldsqr  24201  ofld0le1  24203  metideq  24249  metider  24250  sqsscirc1  24267  esumle  24410  esummono  24411  esumlef  24415  esumcst  24416  aean  24556  dya2ub  24581  dya2icoseg  24588  lgamgulmlem2  24775  lgamgulm2  24781  lgambdd  24782  lgamucov  24783  lgamcvglem  24785  lgamcvg2  24800  gamcvg  24801  subfacval3  24836  sconpht2  24886  sconpi1  24887  rescon  24894  snmlff  24977  sinccvglem  25070  mulge0b  25152  prodmolem2a  25221  faclimlem2  25319  colinearalglem4  25760  axpaschlem  25791  axcontlem7  25821  btwnouttr2  25868  ltflcei  26148  mblfinlem  26151  mblfinlem2  26152  mblfinlem3  26153  volsupnfl  26158  itg2addnclem  26163  itg2addnclem3  26165  iblmulc2nc  26177  bddiblnc  26182  ftc1cnnclem  26185  csbrn  26354  geomcau  26363  bfplem2  26430  rrncmslem  26439  rrnequiv  26442  irrapxlem1  26783  pell1qrgaplem  26834  pell1qrgap  26835  monotoddzzfi  26903  jm2.24nn  26922  congtr  26928  congmul  26930  congsub  26933  fzmaxdif  26944  acongeq  26946  bezoutr1  26949  jm2.20nn  26966  jm2.25  26968  mapfien2  27134  hbtlem4  27206  dgrsub2  27215  mpaaeu  27231  idomsubgmo  27390  dvconstbi  27427  mulltgt0  27568  fmul01  27585  fmul01lt1lem1  27589  fmul01lt1lem2  27590  climrec  27604  climexp  27606  climneg  27611  stoweidlem1  27625  stoweidlem11  27635  stoweidlem13  27637  stoweidlem26  27650  stoweidlem34  27658  stoweidlem38  27662  stoweidlem42  27666  stoweidlem51  27675  stoweidlem59  27683  stirlinglem5  27702  stirlinglem6  27703  stirlinglem7  27704  stirlinglem10  27707  stirlinglem11  27708  stirlinglem12  27709  stirlinglem13  27710  stirlinglem15  27712  isosctrlem1ALT  28765  lsatcvatlem  29544  islshpcv  29548  atlatmstc  29814  cvlsupr7  29843  cvrval3  29907  cvrval5  29909  cvrexchlem  29913  atcvrj1  29925  cvrat3  29936  cvrat4  29937  atbtwn  29940  1cvratex  29967  hlatexch4  29975  3atlem1  29977  3atlem2  29978  atcvrlln2  30013  atcvrlln  30014  lplnllnneN  30050  llncvrlpln2  30051  4atlem3b  30092  lplncvrlvol2  30109  dalemswapyz  30150  dalemswapyzps  30184  dalem25  30192  dalem39  30205  dalem58  30224  dalem59  30225  lneq2at  30272  lncvrat  30276  dalawlem2  30366  dalawlem3  30367  dalawlem4  30368  dalawlem6  30370  dalawlem9  30373  dalawlem11  30375  dalawlem12  30376  lhpocnle  30510  lhpmcvr3  30519  lhpmcvr5N  30521  lhpmcvr6N  30522  4atexlemunv  30560  4atexlemc  30563  4atexlemex2  30565  lautm  30588  cdlemc2  30686  cdleme5  30734  cdleme11j  30761  cdleme16b  30773  cdlemednpq  30793  cdleme19e  30801  cdleme20i  30811  cdleme22a  30834  cdleme22cN  30836  cdleme22d  30837  cdleme22e  30838  cdleme22eALTN  30839  cdleme22f  30840  cdleme23c  30845  cdleme30a  30872  cdleme35a  30942  cdleme35b  30944  cdleme42h  30976  cdlemeg46rgv  31022  cdlemg8b  31122  cdlemg12e  31141  cdlemg13a  31145  cdlemg17pq  31166  cdlemg18c  31174  cdlemg19  31178  cdlemg21  31180  cdlemg31d  31194  cdlemg33a  31200  tendoid  31267  cdlemk4  31328  cdlemki  31335  cdlemk10  31337  cdlemksv2  31341  cdlemk12  31344  cdlemk14  31348  cdlemk15  31349  cdlemk1u  31353  cdlemk5u  31355  cdlemk12u  31366  cdlemk45  31441  cdlemk48  31444  dia2dimlem1  31559  dia2dimlem2  31560  dia2dimlem3  31561  cdlemm10N  31613  cdlemn2  31690  dihjustlem  31711  dihglbcpreN  31795  dihmeetlem3N  31800
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 2393
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 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-rab 2683  df-v 2926  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-sn 3788  df-pr 3789  df-op 3791  df-br 4181
  Copyright terms: Public domain W3C validator