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

Theorem breqtrrd 4198
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 2409 . 2  |-  ( ph  ->  B  =  C )
41, 3breqtrd 4196 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   class class class wbr 4172
This theorem is referenced by:  marypha1lem  7396  marypha2  7402  unxpwdom  7513  uncdadom  8007  cdacomen  8017  cdaassen  8018  xpcdaen  8019  onacda  8033  infcdaabs  8042  cfss  8101  tskuni  8614  ltexnq  8808  xrmax1  10719  xrmax2  10720  max1ALT  10730  qbtwnxr  10742  xleadd1a  10788  xlt2add  10795  xlesubadd  10798  xmulgt0  10818  xlemul1a  10823  xov1plusxeqvd  10997  fzctr  11072  modge0  11212  modlt  11213  modid  11225  sermono  11310  seqf1olem1  11317  seqf1olem2  11318  leexp1a  11393  sqgt0  11405  sqge0  11413  nnlesq  11439  expnbnd  11463  expmulnbnd  11466  discr1  11470  facwordi  11535  faclbnd5  11544  hashdom  11608  brfi1uzind  11670  swrds2  11835  cjmulge0  11906  resqrcl  12014  absge0  12047  sqreulem  12118  amgm2  12128  rlimdm  12300  rlimge0  12330  reccn2  12345  climle  12388  climserle  12411  isercoll2  12417  iseraltlem1  12430  iseralt  12433  isumclim2  12497  isumclim3  12498  isumge0  12505  fsumless  12530  cvgcmp  12550  cvgcmpce  12552  abscvgcvg  12553  isumsup2  12581  isumltss  12583  climcndslem1  12584  climcnds  12586  supcvg  12590  harmonic  12593  expcnv  12598  explecnv  12599  cvgrat  12615  mertenslem1  12616  mertenslem2  12617  efcvg  12642  ege2le3  12647  efaddlem  12650  eftlub  12665  effsumlt  12667  tanhlt1  12716  ef01bndlem  12740  sin02gt0  12748  rpnnen2lem4  12772  ruclem2  12786  ruclem3  12787  ruclem9  12792  iddvdsexp  12828  dvdsadd  12843  dvdsfac  12859  dvdsmod  12861  3dvds  12867  divalglem1  12869  bitsfzo  12902  bitsmod  12903  bitscmp  12905  bitsinv1lem  12908  sadcaddlem  12924  sadadd3  12928  sadaddlem  12933  dvdssqim  13008  dvdsmulgcd  13009  nn0seqcvgd  13016  sqnprm  13053  mulgcddvds  13059  qredeq  13061  isprm6  13064  nonsq  13106  hashdvds  13119  prmdiv  13129  odzdvds  13136  omoe  13141  pythagtriplem4  13148  pcpre1  13171  pcdvdsb  13197  pcz  13209  pcprmpw2  13210  pcaddlem  13212  pcadd  13213  pcadd2  13214  pcmpt  13216  pcmptdvds  13218  fldivp1  13221  pcfaclem  13222  pockthlem  13228  prmreclem1  13239  prmreclem3  13241  prmreclem5  13243  prmreclem6  13244  4sqlem6  13266  4sqlem8  13268  4sqlem11  13278  4sqlem12  13279  4sqlem14  13281  4sqlem16  13283  vdwlem3  13306  vdwlem9  13312  vdwlem10  13313  vdwlem12  13315  ramub1lem2  13350  invfuc  14126  ple1  14428  eqgen  14948  lagsubg  14957  pgpfi  15194  sylow2alem2  15207  sylow2a  15208  sylow3lem4  15219  efgsrel  15321  odadd1  15418  odadd2  15419  gexex  15423  lt6abl  15459  dprd2d2  15557  dmdprdpr  15562  ablfacrp2  15580  ablfac1c  15584  pgpfaclem1  15594  ablfac2  15602  dvdsrmul1  15713  unitmulclb  15725  subrguss  15838  abvres  15882  znfld  16796  znunit  16799  psmetxrge0  18297  isxmet2d  18310  mettri  18335  xmettri3  18336  mettri3  18337  xmetrtri2  18339  prdsxmetlem  18351  imasdsf1olem  18356  xblss2ps  18384  blss2ps  18386  blss2  18387  blssps  18407  blss  18408  prdsbl  18474  dscmet  18573  nmge0  18616  nmmtri  18621  nlmvscnlem2  18674  nrginvrcnlem  18679  nmoix  18716  nmoleub  18718  blcvx  18782  xrsxmet  18793  opnreen  18815  xrge0tsms  18818  icopnfcnv  18920  xrhmeo  18924  lebnumii  18944  pcophtb  19007  pi1grplem  19027  nmoleub2lem  19075  ipcau2  19144  tchcphlem1  19145  ipcau  19148  ipcnlem2  19151  minveclem2  19280  minveclem3b  19282  pjthlem1  19291  pjthlem2  19292  ivthlem3  19303  ivth2  19305  ovolfsf  19321  ovolsslem  19333  ovollb2lem  19337  ovollb2  19338  ovolctb  19339  ovolfiniun  19350  ovolicc1  19365  ovolicc2lem4  19369  ovolicc2  19371  nulmbl2  19384  unmbl  19385  ioombl1lem4  19408  uniioombllem4  19431  uniioombllem6  19433  volivth  19452  vitalilem4  19456  itg1ge0  19531  itg1ge0a  19556  itg1lea  19557  itg1climres  19559  mbfi1fseqlem5  19564  itg2ub  19578  itg2seq  19587  itg2uba  19588  itg2splitlem  19593  itg2split  19594  itg2monolem3  19597  itg2mono  19598  itg2i1fseq2  19601  itg2addlem  19603  iblss  19649  itggt0  19686  dvferm2lem  19823  dvlip  19830  dvivthlem1  19845  dvfsumlem2  19864  dvfsumlem3  19865  ftc1lem4  19876  ply1divmo  20011  ply1remlem  20038  fta1glem2  20042  ig1pdvds  20052  plyeq0lem  20082  plydiveu  20168  fta1lem  20177  vieta1lem2  20181  aaliou3lem2  20213  aaliou3lem8  20215  ulmcn  20268  mtest  20273  itgulm  20277  radcnvlem1  20282  radcnvlt1  20287  dvradcnv  20290  pserdvlem2  20297  abelthlem2  20301  abelthlem6  20305  abelthlem7  20307  abelthlem9  20309  tangtx  20366  sinq12gt0  20368  sineq0  20382  cosordlem  20386  tanord  20393  tanregt0  20394  logrnaddcl  20425  logcj  20454  argregt0  20458  argrege0  20459  argimgt0  20460  argimlt0  20461  logimul  20462  logneg2  20463  logdivlti  20468  divlogrlim  20479  logcnlem3  20488  logcnlem4  20489  dvlog2lem  20496  logtayl  20504  rpcxpcl  20520  cxpsqrlem  20546  cxpaddle  20589  isosctrlem1  20615  asinlem3a  20663  asinlem3  20664  asinneg  20679  asinsinlem  20684  asinsin  20685  atanlogaddlem  20706  atanlogadd  20707  atanlogsublem  20708  atanlogsub  20709  atantan  20716  atanbndlem  20718  atantayl  20730  leibpi  20735  birthdaylem3  20745  areaf  20753  cxploglim  20769  jensenlem2  20779  jensen  20780  logdiflbnd  20786  harmonicbnd4  20802  fsumharmonic  20803  wilthlem2  20805  ftalem1  20808  ftalem2  20809  ftalem5  20812  basellem6  20821  basellem8  20823  basellem9  20824  chtge0  20848  chtublem  20948  logexprlim  20962  perfectlem1  20966  bcmax  21015  bposlem1  21021  bposlem2  21022  bposlem6  21026  bposlem7  21027  lgsdilem2  21068  lgsqrlem4  21081  lgsquadlem1  21091  2sqlem3  21103  2sqlem8  21109  2sqblem  21114  chebbnd1lem2  21117  chtppilimlem1  21120  chtppilim  21122  chto1ub  21123  vmadivsum  21129  rplogsumlem1  21131  rplogsumlem2  21132  dchrisum0lem1a  21133  rpvmasumlem  21134  dchrisumlem1  21136  dchrisumlem2  21137  dchrvmasumlem2  21145  dchrisum0flblem1  21155  dchrisum0flblem2  21156  dchrisum0lem1b  21162  dchrisum0lem1  21163  dchrisum0lem2a  21164  dchrisum0lem3  21166  dchrisum0  21167  mudivsum  21177  mulogsumlem  21178  mulog2sumlem1  21181  mulog2sumlem2  21182  2vmadivsumlem  21187  chpdifbndlem1  21200  selberg3lem1  21204  selberg4lem1  21207  pntrlog2bndlem1  21224  pntrlog2bndlem2  21225  pntrlog2bndlem3  21226  pntrlog2bndlem4  21227  pntpbnd1a  21232  pntpbnd1  21233  pntpbnd2  21234  pntibndlem2  21238  pntibndlem3  21239  pntlemd  21241  pntlemc  21242  pntlemb  21244  pntlemg  21245  pntlemh  21246  pntlemr  21249  pntlemf  21252  pntlemo  21254  abvcxp  21262  ostth2lem1  21265  padicabv  21277  ostth2lem2  21281  ostth2lem3  21282  ostth2lem4  21283  ostth2  21284  ostth3  21285  umgraex  21311  nvabs  22115  nmooge0  22221  nmoolb  22225  siii  22307  minvecolem2  22330  minvecolem4  22335  minvecolem5  22336  hlipgt0  22369  normge0  22581  normpyc  22601  pjhthlem1  22846  pjige0i  23145  nmoplb  23363  nmfnlb  23380  branmfn  23561  pjssdif2i  23630  stlei  23696  xlt2addrd  24077  eliccelico  24093  elicoelioo  24094  bcm1n  24104  xrge0tsmsd  24176  ofldchr  24197  xrge0iifiso  24274  gsumesum  24404  esumcst  24408  esumpcvgval  24421  esumcvg  24429  measssd  24522  measunl  24523  sibfof  24607  ballotlemsgt1  24721  ballotlemsel1i  24723  zetacvg  24752  lgamgulmlem2  24767  lgamgulmlem3  24768  lgamcvg2  24792  subfaclim  24827  erdszelem7  24836  erdszelem8  24837  cvmliftlem2  24926  snmlff  24969  sinccvglem  25062  climlec3  25167  clim2div  25170  ntrivcvgtail  25181  iprodclim2  25265  iprodclim3  25266  faclim  25313  dvdspw  25317  nodense  25557  nobndup  25568  axpaschlem  25783  axcontlem8  25814  lxflflp1  26142  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  itg2addnclem  26155  itg2addnclem3  26157  itg2gt0cn  26159  itggt0cn  26176  fnejoin1  26287  isbnd3  26383  ssbnd  26387  heiborlem8  26417  bfplem2  26422  rrncmslem  26431  rrnequiv  26434  rrntotbnd  26435  eldioph2lem1  26708  lzenom  26718  irrapxlem1  26775  irrapxlem4  26778  irrapxlem5  26779  pell14qrgt0  26812  pell1qrge1  26823  pell1qrgap  26827  pellfundge  26835  pellfundex  26839  pellfund14  26851  rmspecsqrnq  26859  rmxypos  26902  ltrmynn0  26903  ltrmxnn0  26904  jm2.24nn  26914  jm2.17b  26916  jm2.17c  26917  jm2.24  26918  congadd  26921  congsym  26923  congneg  26924  congid  26926  mzpcong  26927  acongrep  26935  acongeq  26938  jm2.18  26949  jm2.19  26954  jm2.23  26957  jm2.25  26960  jm2.26lem3  26962  jm2.15nn0  26964  jm2.16nn0  26965  jm2.27a  26966  jm2.27c  26968  jm3.1lem1  26978  idomrootle  27379  idomsubgmo  27382  cncmpmax  27570  fmul01  27577  fmul01lt1lem1  27581  climdivf  27605  stoweidlem1  27617  stoweidlem16  27632  stoweidlem18  27634  stoweidlem24  27640  stoweidlem26  27642  stoweidlem36  27652  stoweidlem38  27654  stoweidlem41  27657  stoweidlem42  27658  stoweidlem44  27660  stoweidlem45  27661  stoweidlem48  27664  stoweidlem62  27678  wallispilem5  27685  stirlinglem1  27690  stirlinglem5  27694  stirlinglem7  27696  stirlinglem8  27697  stirlinglem9  27698  stirlinglem11  27700  rlimdmafv  27908  lcv1  29524  lsatcv0eq  29530  lsatcvat3  29535  cvlsupr2  29826  hlatlej2  29858  cvrval4N  29896  cvratlem  29903  atcvr0eq  29908  2atlt  29921  atbtwnex  29930  athgt  29938  1cvrat  29958  ps-1  29959  hlatexch3N  29962  hlatexch4  29963  3atlem2  29966  atcvrlln2  30001  lplnexllnN  30046  4atlem3a  30079  4atlem10b  30087  4atlem11b  30090  4atlem12b  30093  2lplnja  30101  dalemply  30136  dalemsly  30137  dalem1  30141  dalem6  30150  dalem7  30151  dalem-cly  30153  dalem11  30156  dalem12  30157  dalem16  30161  dalem17  30162  dalem38  30192  dalem44  30198  dalem61  30215  lnatexN  30261  lncvrat  30264  lncmp  30265  paddasslem2  30303  dalawlem3  30355  dalawlem6  30358  dalawlem11  30363  lhpmcvr  30505  lhp2atne  30516  lhp2at0ne  30518  lautj  30575  trlval4  30670  cdlemc2  30674  cdlemc5  30677  cdleme3b  30711  cdleme11c  30743  cdleme19a  30785  cdleme20j  30800  cdleme22f  30828  cdleme23c  30833  cdleme26f2ALTN  30846  cdleme26f2  30847  cdleme35fnpq  30931  cdleme48bw  30984  cdlemg10a  31122  cdlemg11b  31124  cdlemg17g  31149  cdlemg18c  31162  cdlemi1  31300  cdlemk52  31436  dia2dimlem1  31547  dihord1  31701  dihjatcclem4  31904
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 2385
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 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173
  Copyright terms: Public domain W3C validator