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

Theorem breqtrrd 4230
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
Hypotheses
Ref Expression
breqtrrd.1  |-  ( ph  ->  A R B )
breqtrrd.2  |-  ( ph  ->  C  =  B )
Assertion
Ref Expression
breqtrrd  |-  ( ph  ->  A R C )

Proof of Theorem breqtrrd
StepHypRef Expression
1 breqtrrd.1 . 2  |-  ( ph  ->  A R B )
2 breqtrrd.2 . . 3  |-  ( ph  ->  C  =  B )
32eqcomd 2440 . 2  |-  ( ph  ->  B  =  C )
41, 3breqtrd 4228 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   class class class wbr 4204
This theorem is referenced by:  marypha1lem  7429  marypha2  7435  unxpwdom  7546  uncdadom  8040  cdacomen  8050  cdaassen  8051  xpcdaen  8052  onacda  8066  infcdaabs  8075  cfss  8134  tskuni  8647  ltexnq  8841  xrmax1  10752  xrmax2  10753  max1ALT  10763  qbtwnxr  10775  xleadd1a  10821  xlt2add  10828  xlesubadd  10831  xmulgt0  10851  xlemul1a  10856  xov1plusxeqvd  11030  fzctr  11105  modge0  11245  modlt  11246  modid  11258  sermono  11343  seqf1olem1  11350  seqf1olem2  11351  leexp1a  11426  sqgt0  11438  sqge0  11446  nnlesq  11472  expnbnd  11496  expmulnbnd  11499  discr1  11503  facwordi  11568  faclbnd5  11577  hashdom  11641  brfi1uzind  11703  swrds2  11868  cjmulge0  11939  resqrcl  12047  absge0  12080  sqreulem  12151  amgm2  12161  rlimdm  12333  rlimge0  12363  reccn2  12378  climle  12421  climserle  12444  isercoll2  12450  iseraltlem1  12463  iseralt  12466  isumclim2  12530  isumclim3  12531  isumge0  12538  fsumless  12563  cvgcmp  12583  cvgcmpce  12585  abscvgcvg  12586  isumsup2  12614  isumltss  12616  climcndslem1  12617  climcnds  12619  supcvg  12623  harmonic  12626  expcnv  12631  explecnv  12632  cvgrat  12648  mertenslem1  12649  mertenslem2  12650  efcvg  12675  ege2le3  12680  efaddlem  12683  eftlub  12698  effsumlt  12700  tanhlt1  12749  ef01bndlem  12773  sin02gt0  12781  rpnnen2lem4  12805  ruclem2  12819  ruclem3  12820  ruclem9  12825  iddvdsexp  12861  dvdsadd  12876  dvdsfac  12892  dvdsmod  12894  3dvds  12900  divalglem1  12902  bitsfzo  12935  bitsmod  12936  bitscmp  12938  bitsinv1lem  12941  sadcaddlem  12957  sadadd3  12961  sadaddlem  12966  dvdssqim  13041  dvdsmulgcd  13042  nn0seqcvgd  13049  sqnprm  13086  mulgcddvds  13092  qredeq  13094  isprm6  13097  nonsq  13139  hashdvds  13152  prmdiv  13162  odzdvds  13169  omoe  13174  pythagtriplem4  13181  pcpre1  13204  pcdvdsb  13230  pcz  13242  pcprmpw2  13243  pcaddlem  13245  pcadd  13246  pcadd2  13247  pcmpt  13249  pcmptdvds  13251  fldivp1  13254  pcfaclem  13255  pockthlem  13261  prmreclem1  13272  prmreclem3  13274  prmreclem5  13276  prmreclem6  13277  4sqlem6  13299  4sqlem8  13301  4sqlem11  13311  4sqlem12  13312  4sqlem14  13314  4sqlem16  13316  vdwlem3  13339  vdwlem9  13345  vdwlem10  13346  vdwlem12  13348  ramub1lem2  13383  invfuc  14159  ple1  14461  eqgen  14981  lagsubg  14990  pgpfi  15227  sylow2alem2  15240  sylow2a  15241  sylow3lem4  15252  efgsrel  15354  odadd1  15451  odadd2  15452  gexex  15456  lt6abl  15492  dprd2d2  15590  dmdprdpr  15595  ablfacrp2  15613  ablfac1c  15617  pgpfaclem1  15627  ablfac2  15635  dvdsrmul1  15746  unitmulclb  15758  subrguss  15871  abvres  15915  znfld  16829  znunit  16832  psmetxrge0  18332  isxmet2d  18345  mettri  18370  xmettri3  18371  mettri3  18372  xmetrtri2  18374  prdsxmetlem  18386  imasdsf1olem  18391  xblss2ps  18419  blss2ps  18421  blss2  18422  blssps  18442  blss  18443  prdsbl  18509  dscmet  18608  nmge0  18651  nmmtri  18656  nlmvscnlem2  18709  nrginvrcnlem  18714  nmoix  18751  nmoleub  18753  blcvx  18817  xrsxmet  18828  opnreen  18850  xrge0tsms  18853  icopnfcnv  18955  xrhmeo  18959  lebnumii  18979  pcophtb  19042  pi1grplem  19062  nmoleub2lem  19110  ipcau2  19179  tchcphlem1  19180  ipcau  19183  ipcnlem2  19186  minveclem2  19315  minveclem3b  19317  pjthlem1  19326  pjthlem2  19327  ivthlem3  19338  ivth2  19340  ovolfsf  19356  ovolsslem  19368  ovollb2lem  19372  ovollb2  19373  ovolctb  19374  ovolfiniun  19385  ovolicc1  19400  ovolicc2lem4  19404  ovolicc2  19406  nulmbl2  19419  unmbl  19420  ioombl1lem4  19443  uniioombllem4  19466  uniioombllem6  19468  volivth  19487  vitalilem4  19491  itg1ge0  19566  itg1ge0a  19591  itg1lea  19592  itg1climres  19594  mbfi1fseqlem5  19599  itg2ub  19613  itg2seq  19622  itg2uba  19623  itg2splitlem  19628  itg2split  19629  itg2monolem3  19632  itg2mono  19633  itg2i1fseq2  19636  itg2addlem  19638  iblss  19684  itggt0  19721  dvferm2lem  19858  dvlip  19865  dvivthlem1  19880  dvfsumlem2  19899  dvfsumlem3  19900  ftc1lem4  19911  ply1divmo  20046  ply1remlem  20073  fta1glem2  20077  ig1pdvds  20087  plyeq0lem  20117  plydiveu  20203  fta1lem  20212  vieta1lem2  20216  aaliou3lem2  20248  aaliou3lem8  20250  ulmcn  20303  mtest  20308  itgulm  20312  radcnvlem1  20317  radcnvlt1  20322  dvradcnv  20325  pserdvlem2  20332  abelthlem2  20336  abelthlem6  20340  abelthlem7  20342  abelthlem9  20344  tangtx  20401  sinq12gt0  20403  sineq0  20417  cosordlem  20421  tanord  20428  tanregt0  20429  logrnaddcl  20460  logcj  20489  argregt0  20493  argrege0  20494  argimgt0  20495  argimlt0  20496  logimul  20497  logneg2  20498  logdivlti  20503  divlogrlim  20514  logcnlem3  20523  logcnlem4  20524  dvlog2lem  20531  logtayl  20539  rpcxpcl  20555  cxpsqrlem  20581  cxpaddle  20624  isosctrlem1  20650  asinlem3a  20698  asinlem3  20699  asinneg  20714  asinsinlem  20719  asinsin  20720  atanlogaddlem  20741  atanlogadd  20742  atanlogsublem  20743  atanlogsub  20744  atantan  20751  atanbndlem  20753  atantayl  20765  leibpi  20770  birthdaylem3  20780  areaf  20788  cxploglim  20804  jensenlem2  20814  jensen  20815  logdiflbnd  20821  harmonicbnd4  20837  fsumharmonic  20838  wilthlem2  20840  ftalem1  20843  ftalem2  20844  ftalem5  20847  basellem6  20856  basellem8  20858  basellem9  20859  chtge0  20883  chtublem  20983  logexprlim  20997  perfectlem1  21001  bcmax  21050  bposlem1  21056  bposlem2  21057  bposlem6  21061  bposlem7  21062  lgsdilem2  21103  lgsqrlem4  21116  lgsquadlem1  21126  2sqlem3  21138  2sqlem8  21144  2sqblem  21149  chebbnd1lem2  21152  chtppilimlem1  21155  chtppilim  21157  chto1ub  21158  vmadivsum  21164  rplogsumlem1  21166  rplogsumlem2  21167  dchrisum0lem1a  21168  rpvmasumlem  21169  dchrisumlem1  21171  dchrisumlem2  21172  dchrvmasumlem2  21180  dchrisum0flblem1  21190  dchrisum0flblem2  21191  dchrisum0lem1b  21197  dchrisum0lem1  21198  dchrisum0lem2a  21199  dchrisum0lem3  21201  dchrisum0  21202  mudivsum  21212  mulogsumlem  21213  mulog2sumlem1  21216  mulog2sumlem2  21217  2vmadivsumlem  21222  chpdifbndlem1  21235  selberg3lem1  21239  selberg4lem1  21242  pntrlog2bndlem1  21259  pntrlog2bndlem2  21260  pntrlog2bndlem3  21261  pntrlog2bndlem4  21262  pntpbnd1a  21267  pntpbnd1  21268  pntpbnd2  21269  pntibndlem2  21273  pntibndlem3  21274  pntlemd  21276  pntlemc  21277  pntlemb  21279  pntlemg  21280  pntlemh  21281  pntlemr  21284  pntlemf  21287  pntlemo  21289  abvcxp  21297  ostth2lem1  21300  padicabv  21312  ostth2lem2  21316  ostth2lem3  21317  ostth2lem4  21318  ostth2  21319  ostth3  21320  umgraex  21346  nvabs  22150  nmooge0  22256  nmoolb  22260  siii  22342  minvecolem2  22365  minvecolem4  22370  minvecolem5  22371  hlipgt0  22404  normge0  22616  normpyc  22636  pjhthlem1  22881  pjige0i  23180  nmoplb  23398  nmfnlb  23415  branmfn  23596  pjssdif2i  23665  stlei  23731  xlt2addrd  24112  eliccelico  24128  elicoelioo  24129  bcm1n  24139  xrge0tsmsd  24211  ofldchr  24232  xrge0iifiso  24309  gsumesum  24439  esumcst  24443  esumpcvgval  24456  esumcvg  24464  measssd  24557  measunl  24558  sibfof  24642  ballotlemsgt1  24756  ballotlemsel1i  24758  zetacvg  24787  lgamgulmlem2  24802  lgamgulmlem3  24803  lgamcvg2  24827  subfaclim  24862  erdszelem7  24871  erdszelem8  24872  cvmliftlem2  24961  snmlff  25004  sinccvglem  25097  climlec3  25202  clim2div  25206  ntrivcvgtail  25217  iprodclim2  25301  iprodclim3  25302  faclim  25354  dvdspw  25358  nodense  25598  nobndup  25609  axpaschlem  25827  axcontlem8  25858  lxflflp1  26189  mblfinlem  26190  mblfinlem2  26191  mblfinlem3  26192  ismblfin  26193  itg2addnclem  26202  itg2addnclem3  26204  itg2gt0cn  26206  itggt0cn  26223  fnejoin1  26334  isbnd3  26430  ssbnd  26434  heiborlem8  26464  bfplem2  26469  rrncmslem  26478  rrnequiv  26481  rrntotbnd  26482  eldioph2lem1  26755  lzenom  26765  irrapxlem1  26822  irrapxlem4  26825  irrapxlem5  26826  pell14qrgt0  26859  pell1qrge1  26870  pell1qrgap  26874  pellfundge  26882  pellfundex  26886  pellfund14  26898  rmspecsqrnq  26906  rmxypos  26949  ltrmynn0  26950  ltrmxnn0  26951  jm2.24nn  26961  jm2.17b  26963  jm2.17c  26964  jm2.24  26965  congadd  26968  congsym  26970  congneg  26971  congid  26973  mzpcong  26974  acongrep  26982  acongeq  26985  jm2.18  26996  jm2.19  27001  jm2.23  27004  jm2.25  27007  jm2.26lem3  27009  jm2.15nn0  27011  jm2.16nn0  27012  jm2.27a  27013  jm2.27c  27015  jm3.1lem1  27025  idomrootle  27426  idomsubgmo  27429  cncmpmax  27617  fmul01  27624  fmul01lt1lem1  27628  climdivf  27652  stoweidlem1  27664  stoweidlem16  27679  stoweidlem18  27681  stoweidlem24  27687  stoweidlem26  27689  stoweidlem36  27699  stoweidlem38  27701  stoweidlem41  27704  stoweidlem42  27705  stoweidlem44  27707  stoweidlem45  27708  stoweidlem48  27711  stoweidlem62  27725  wallispilem5  27732  stirlinglem1  27737  stirlinglem5  27741  stirlinglem7  27743  stirlinglem8  27744  stirlinglem9  27745  stirlinglem11  27747  rlimdmafv  27955  shwrdidx  28130  shwrdidx0  28132  2shwrd1lem1  28136  2shwrd1lem2  28137  lcv1  29678  lsatcv0eq  29684  lsatcvat3  29689  cvlsupr2  29980  hlatlej2  30012  cvrval4N  30050  cvratlem  30057  atcvr0eq  30062  2atlt  30075  atbtwnex  30084  athgt  30092  1cvrat  30112  ps-1  30113  hlatexch3N  30116  hlatexch4  30117  3atlem2  30120  atcvrlln2  30155  lplnexllnN  30200  4atlem3a  30233  4atlem10b  30241  4atlem11b  30244  4atlem12b  30247  2lplnja  30255  dalemply  30290  dalemsly  30291  dalem1  30295  dalem6  30304  dalem7  30305  dalem-cly  30307  dalem11  30310  dalem12  30311  dalem16  30315  dalem17  30316  dalem38  30346  dalem44  30352  dalem61  30369  lnatexN  30415  lncvrat  30418  lncmp  30419  paddasslem2  30457  dalawlem3  30509  dalawlem6  30512  dalawlem11  30517  lhpmcvr  30659  lhp2atne  30670  lhp2at0ne  30672  lautj  30729  trlval4  30824  cdlemc2  30828  cdlemc5  30831  cdleme3b  30865  cdleme11c  30897  cdleme19a  30939  cdleme20j  30954  cdleme22f  30982  cdleme23c  30987  cdleme26f2ALTN  31000  cdleme26f2  31001  cdleme35fnpq  31085  cdleme48bw  31138  cdlemg10a  31276  cdlemg11b  31278  cdlemg17g  31303  cdlemg18c  31316  cdlemi1  31454  cdlemk52  31590  dia2dimlem1  31701  dihord1  31855  dihjatcclem4  32058
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 2416
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 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205
  Copyright terms: Public domain W3C validator