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

Theorem breqtrd 4236
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 4224 . 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 1652   class class class wbr 4212
This theorem is referenced by:  breqtrrd  4238  syl5breq  4247  domunsn  7257  mapdom2  7278  phplem4  7289  wemaplem2  7516  infdifsn  7611  cantnff  7629  infxpenlem  7895  pwcda1  8074  pwcdadom  8096  infmap2  8098  ssfin4  8190  canthp1lem1  8527  nqereq  8812  ltexnq  8852  ltbtwnnq  8855  add20  9540  mullt0  9547  ltm1  9850  recgt0  9854  prodgt0  9855  prodge0  9857  ltmul1a  9859  recp1lt1  9908  recreclt  9909  ledivp1  9912  ledivp1i  9936  ltdivp1i  9937  ltaddrp2d  10678  xleadd1a  10832  xov1plusxeqvd  11041  fz01en  11079  fladdz  11227  flhalf  11231  fldiv  11241  modsubdir  11285  fzen2  11308  serle  11378  ltexp2a  11431  leexp2a  11435  exple1  11439  expubnd  11440  bernneq  11505  expmulnbnd  11511  discr1  11515  discr  11516  faclbnd6  11590  hashfz  11692  hashfun  11700  seqcoll  11712  sqeqd  11971  sqrlem7  12054  sqrge0  12063  sqrneglem  12072  abslt  12118  absle  12119  abstri  12134  rlimge0  12375  reccn2  12390  climaddc2  12429  isercolllem1  12458  caucvgrlem  12466  summolem2a  12509  isumge0  12550  fsumle  12578  fsumlt  12579  o1fsum  12592  supcvg  12635  expcnv  12643  geolim  12647  geolim2  12648  georeclim  12649  geo2lim  12652  mertenslem1  12661  mertens  12663  efcllem  12680  ef0lem  12681  efgt0  12704  eftlub  12710  eflt  12718  sinbnd  12781  cosbnd  12782  ef01bndlem  12785  sin01gt0  12791  cos01gt0  12792  sin02gt0  12793  eirrlem  12803  rpnnen2lem11  12824  rpnnen2  12825  ruclem11  12839  dvdssub2  12887  dvdsadd2b  12892  dvdsexp  12905  3dvds  12912  bitsfzolem  12946  bitsinv1lem  12953  bezoutlem4  13041  dvdsgcd  13043  dvdsmulgcd  13054  nn0seqcvgd  13061  prmind2  13090  rpmulgcd2  13105  qredeq  13106  rpdvds  13124  divdenle  13141  hashdvds  13164  phimullem  13168  eulerthlem2  13171  prmdiveq  13175  prmdivdiv  13176  opoe  13185  pythagtriplem4  13193  pythagtriplem10  13194  pythagtriplem19  13207  iserodd  13209  pcpre1  13216  pcadd2  13259  qexpz  13270  expnprm  13271  pockthlem  13273  prmreclem2  13285  prmreclem3  13286  4sqlem7  13312  4sqlem10  13315  4sqlem11  13323  4sqlem12  13324  4sqlem14  13326  4sqlem15  13327  4sqlem16  13328  0ram  13388  ffthiso  14126  latmlej12  14520  divsgrp  14995  pgpfi1  15229  sylow1lem4  15235  sylow1lem5  15236  odcau  15238  pgpfi  15239  pgpssslw  15248  sylow3lem4  15264  sylow3lem6  15266  efgsfo  15371  frgp0  15392  odadd1  15463  odadd2  15464  odadd  15465  gexexlem  15467  lt6abl  15504  dprd2dlem1  15599  dprd2d2  15602  ablfacrplem  15623  ablfacrp  15624  ablfacrp2  15625  ablfac1b  15628  ablfac1eu  15631  pgpfac1lem3a  15634  ablfaclem2  15644  dvdsrid  15756  dvdsrtr  15757  dvdsrneg  15759  unitmulcl  15769  unitgrp  15772  unitnegcl  15786  isdrng2  15845  subrguss  15883  subrgunit  15886  abvsubtri  15923  fidomndrnglem  16366  psrbaglesupp  16433  gzrngunit  16764  prmirredlem  16773  znidomb  16842  psmetsym  18341  psmettri  18342  mettri2  18371  xmetsym  18377  xmettri  18381  prdsxmetlem  18398  xblss2ps  18431  xblss2  18432  blhalf  18435  xmsge0  18493  ngptgp  18677  nrginvrcnlem  18726  nmoeq0  18770  cnmet  18806  blcvx  18829  opnreen  18862  metdcnlem  18867  metdstri  18881  metdsle  18882  metnrmlem1  18889  metnrmlem3  18891  lebnumlem1  18986  pi1inv  19077  cphnmf  19158  ipge0  19161  ipcau2  19191  tchcphlem1  19192  minveclem2  19327  minveclem3  19330  ovolssnul  19383  ovolctb  19386  ovolunnul  19396  ovoliunlem1  19398  ovoliun2  19402  ovoliunnul  19403  ioombl1lem4  19455  uniioombllem3  19477  uniioombllem4  19478  uniioombllem5  19479  uniioombl  19481  volcn  19498  vitalilem2  19501  vitalilem5  19504  itg1lea  19604  mbfi1fseqlem6  19612  mbfi1flimlem  19614  itg2eqa  19637  itg2splitlem  19640  itg2split  19641  itg2monolem1  19642  itg2cnlem2  19654  iblabsr  19721  iblmulc2  19722  dveflem  19863  dvef  19864  dvferm2lem  19870  dvlip  19877  c1liplem1  19880  dveq0  19884  dvlt0  19889  dvivthlem1  19892  lhop1  19898  dvfsumle  19905  dvfsumlem4  19913  dvfsumrlim3  19917  dvfsum2  19918  ftc1a  19921  ftc1lem4  19923  deg1add  20026  ply1divex  20059  ply1rem  20086  fta1glem2  20089  fta1blem  20091  ig1pdvds  20099  plyeq0lem  20129  dgrcolem2  20192  plydivlem4  20213  plyrem  20222  fta1lem  20224  aalioulem3  20251  aaliou2b  20258  aaliou3lem3  20261  aaliou3lem8  20262  ulmcn  20315  ulmdvlem1  20316  itgulm  20324  pserulm  20338  pserdvlem2  20344  abelthlem2  20348  abelthlem5  20351  abelthlem6  20352  abelthlem7  20354  abelthlem8  20355  abelthlem9  20356  sinq12gt0  20415  sinq34lt0t  20417  cosq14gt0  20418  cosq14ge0  20419  efif1olem3  20446  argimgt0  20507  argimlt0  20508  logneg2  20510  logcnlem3  20535  logcnlem4  20536  logtayllem  20550  logtayl2  20553  cxpsqrlem  20593  cxpsqr  20594  cxpaddlelem  20635  abscxpbnd  20637  loglesqr  20642  ang180lem2  20652  atanlogaddlem  20753  atanlogsublem  20755  atantan  20763  atans2  20771  atantayl  20777  leibpi  20782  log2tlbnd  20785  birthdaylem2  20791  birthdaylem3  20792  cxp2limlem  20814  jensenlem2  20826  jensen  20827  logdiflbnd  20833  emcllem2  20835  emcllem4  20837  harmonicbnd4  20849  fsumharmonic  20850  wilthlem3  20853  basellem1  20863  basellem3  20865  basellem4  20866  fsumdvdsdiaglem  20968  dvdsppwf1o  20971  dvdsmulf1o  20979  chteq0  20993  chtub  20996  chpub  21004  logfacubnd  21005  logfaclbnd  21006  logexprlim  21009  perfectlem2  21014  dchrfi  21039  bclbnd  21064  bposlem1  21068  bposlem3  21070  bposlem4  21071  bposlem6  21073  lgslem1  21080  lgsqrlem2  21126  lgsqrlem4  21128  lgseisenlem2  21134  lgsquadlem1  21138  lgsquadlem2  21139  lgsquad2lem1  21142  2sqlem3  21150  2sqlem4  21151  2sqlem8  21156  2sqlem11  21159  chebbnd1lem2  21164  chebbnd1lem3  21165  chtppilimlem1  21167  chpchtlim  21173  vmadivsum  21176  vmadivsumb  21177  rpvmasumlem  21181  dchrisumlem2  21184  dchrmusum2  21188  dchrvmasumlem2  21192  dchrvmasumlem3  21193  dchrisum0flblem2  21203  dchrisum0fno1  21205  dchrisum0re  21207  dchrisum0lem1  21210  dchrisum0lem2a  21211  mudivsum  21224  mulogsumlem  21225  mulog2sumlem2  21229  vmalogdivsum2  21232  selberglem2  21240  selbergb  21243  selberg2b  21246  logdivbnd  21250  selberg3lem1  21251  selberg3lem2  21252  selberg4lem1  21254  pntrmax  21258  pntrlog2bndlem2  21272  pntrlog2bndlem3  21273  pntrlog2bndlem5  21275  pntrlog2bndlem6a  21276  pntrlog2bndlem6  21277  pntrlog2bnd  21278  pntpbnd1a  21279  pntpbnd1  21280  pntpbnd2  21281  pntibndlem1  21283  pntibndlem2  21285  pntlemb  21291  pntlemq  21295  pntlemr  21296  pntlemj  21297  pntlemk  21300  qabvle  21319  padicabvcxp  21326  ostth2lem2  21328  ostth2lem3  21329  ostth2lem4  21330  ostth3  21332  nvge0  22163  smcnlem  22193  nmoub3i  22274  nmoub2i  22275  nmlno0lem  22294  minvecolem2  22377  htthlem  22420  norm3dif2  22653  bcs2  22684  chscllem2  23140  eigposi  23339  nmopub2tALT  23412  nmfnleub2  23429  nmlnop0iALT  23498  riesz1  23568  cnlnadjlem2  23571  nmopcoadji  23604  leopsq  23632  leopmul  23637  leopnmid  23641  nmopleid  23642  opsqrlem6  23648  0leopj  23689  hstle1  23729  strlem3a  23755  mdslmd4i  23836  cvexchlem  23871  cdj1i  23936  le2halvesd  24122  xlt2addrd  24124  xrge0tsmsd  24223  ofldsqr  24240  ofld0le1  24242  metideq  24288  metider  24289  sqsscirc1  24306  esumle  24449  esummono  24450  esumlef  24454  esumcst  24455  aean  24595  dya2ub  24620  dya2icoseg  24627  lgamgulmlem2  24814  lgamgulm2  24820  lgambdd  24821  lgamucov  24822  lgamcvglem  24824  lgamcvg2  24839  gamcvg  24840  subfacval3  24875  sconpht2  24925  sconpi1  24926  rescon  24933  snmlff  25016  sinccvglem  25109  mulge0b  25191  prodmolem2a  25260  faclimlem2  25363  colinearalglem4  25848  axpaschlem  25879  axcontlem7  25909  btwnouttr2  25956  ltflcei  26239  mblfinlem2  26244  mblfinlem3  26245  mblfinlem4  26246  volsupnfl  26251  itg2addnclem  26256  itg2addnclem3  26258  iblmulc2nc  26270  bddiblnc  26275  ftc1cnnclem  26278  ftc1anclem6  26285  ftc1anclem7  26286  ftc1anclem8  26287  ftc2nc  26289  csbrn  26456  geomcau  26465  bfplem2  26532  rrncmslem  26541  rrnequiv  26544  irrapxlem1  26885  pell1qrgaplem  26936  pell1qrgap  26937  monotoddzzfi  27005  jm2.24nn  27024  congtr  27030  congmul  27032  congsub  27035  fzmaxdif  27046  acongeq  27048  bezoutr1  27051  jm2.20nn  27068  jm2.25  27070  mapfien2  27235  hbtlem4  27307  dgrsub2  27316  mpaaeu  27332  idomsubgmo  27491  dvconstbi  27528  mulltgt0  27669  fmul01  27686  fmul01lt1lem1  27690  fmul01lt1lem2  27691  climrec  27705  climexp  27707  climneg  27712  stoweidlem1  27726  stoweidlem11  27736  stoweidlem13  27738  stoweidlem26  27751  stoweidlem34  27759  stoweidlem38  27763  stoweidlem42  27767  stoweidlem51  27776  stoweidlem59  27784  stirlinglem5  27803  stirlinglem6  27804  stirlinglem7  27805  stirlinglem10  27808  stirlinglem11  27809  stirlinglem12  27810  stirlinglem13  27811  stirlinglem15  27813  fzonmapblen  28134  isosctrlem1ALT  29046  lsatcvatlem  29847  islshpcv  29851  atlatmstc  30117  cvlsupr7  30146  cvrval3  30210  cvrval5  30212  cvrexchlem  30216  atcvrj1  30228  cvrat3  30239  cvrat4  30240  atbtwn  30243  1cvratex  30270  hlatexch4  30278  3atlem1  30280  3atlem2  30281  atcvrlln2  30316  atcvrlln  30317  lplnllnneN  30353  llncvrlpln2  30354  4atlem3b  30395  lplncvrlvol2  30412  dalemswapyz  30453  dalemswapyzps  30487  dalem25  30495  dalem39  30508  dalem58  30527  dalem59  30528  lneq2at  30575  lncvrat  30579  dalawlem2  30669  dalawlem3  30670  dalawlem4  30671  dalawlem6  30673  dalawlem9  30676  dalawlem11  30678  dalawlem12  30679  lhpocnle  30813  lhpmcvr3  30822  lhpmcvr5N  30824  lhpmcvr6N  30825  4atexlemunv  30863  4atexlemc  30866  4atexlemex2  30868  lautm  30891  cdlemc2  30989  cdleme5  31037  cdleme11j  31064  cdleme16b  31076  cdlemednpq  31096  cdleme19e  31104  cdleme20i  31114  cdleme22a  31137  cdleme22cN  31139  cdleme22d  31140  cdleme22e  31141  cdleme22eALTN  31142  cdleme22f  31143  cdleme23c  31148  cdleme30a  31175  cdleme35a  31245  cdleme35b  31247  cdleme42h  31279  cdlemeg46rgv  31325  cdlemg8b  31425  cdlemg12e  31444  cdlemg13a  31448  cdlemg17pq  31469  cdlemg18c  31477  cdlemg19  31481  cdlemg21  31483  cdlemg31d  31497  cdlemg33a  31503  tendoid  31570  cdlemk4  31631  cdlemki  31638  cdlemk10  31640  cdlemksv2  31644  cdlemk12  31647  cdlemk14  31651  cdlemk15  31652  cdlemk1u  31656  cdlemk5u  31658  cdlemk12u  31669  cdlemk45  31744  cdlemk48  31747  dia2dimlem1  31862  dia2dimlem2  31863  dia2dimlem3  31864  cdlemm10N  31916  cdlemn2  31993  dihjustlem  32014  dihglbcpreN  32098  dihmeetlem3N  32103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-br 4213
  Copyright terms: Public domain W3C validator