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

Theorem 3brtr4d 4054
Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005.)
Hypotheses
Ref Expression
3brtr4d.1  |-  ( ph  ->  A R B )
3brtr4d.2  |-  ( ph  ->  C  =  A )
3brtr4d.3  |-  ( ph  ->  D  =  B )
Assertion
Ref Expression
3brtr4d  |-  ( ph  ->  C R D )

Proof of Theorem 3brtr4d
StepHypRef Expression
1 3brtr4d.1 . 2  |-  ( ph  ->  A R B )
2 3brtr4d.2 . . 3  |-  ( ph  ->  C  =  A )
3 3brtr4d.3 . . 3  |-  ( ph  ->  D  =  B )
42, 3breq12d 4037 . 2  |-  ( ph  ->  ( C R D  <-> 
A R B ) )
51, 4mpbird 223 1  |-  ( ph  ->  C R D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   class class class wbr 4024
This theorem is referenced by:  f1oiso2  5811  sucdom2  7053  ordtypelem6  7234  cdaen  7795  cdacomen  7803  cdadom1  7808  fin23lem26  7947  distrnq  8581  lediv12a  9645  recp1lt1  9650  ifle  10520  xleadd1a  10569  xlemul1a  10604  quoremz  10955  quoremnn0  10957  intfracq  10959  modmulnn  10984  fzennn  11026  monoord2  11073  expgt1  11136  leexp2r  11155  leexp1a  11156  bernneq  11223  expmulnbnd  11229  digit1  11231  faclbnd  11299  faclbnd4lem3  11304  faclbnd4lem4  11305  faclbnd6  11308  facubnd  11309  hashdomi  11358  fzsdom2  11378  absrele  11789  absimle  11790  abstri  11810  abs2difabs  11814  limsupval2  11950  rlimrege0  12049  rlimrecl  12050  climsqz  12110  climsqz2  12111  rlimdiv  12115  rlimsqz  12119  rlimsqz2  12120  isercolllem1  12134  isercoll2  12138  fsumcvg2  12196  fsumrlim  12265  o1fsum  12267  cvgcmpce  12272  isumle  12299  climcndslem1  12304  climcndslem2  12305  harmonic  12313  expcnv  12318  explecnv  12319  geomulcvg  12328  efcllem  12355  ege2le3  12367  eflegeo  12397  rpnnen2lem4  12492  ruclem2  12506  ruclem8  12511  fsumdvds  12568  phibnd  12835  iserodd  12884  pcdvdstr  12924  pcprmpw2  12930  pockthg  12949  prmreclem4  12962  2expltfac  13101  mod2ile  14208  odsubdvds  14878  pgpfi  14912  fislw  14932  efgredlemd  15049  efgredlem  15052  frgpcpbl  15064  abvres  15600  abvtrivd  15601  znrrg  16515  xmetge0  17905  xmetres2  17921  imasf1oxmet  17935  comet  18055  stdbdxmet  18057  dscmet  18091  nrmmetd  18093  nmrtri  18141  tngngp  18166  nmolb2d  18223  nmoleub  18236  nmoco  18242  nmotri  18244  nmoid  18247  nmods  18249  cnmet  18277  xrsxmet  18311  metdstri  18351  metnrmlem3  18361  lebnumlem3  18457  ipcau2  18660  tchcphlem1  18661  tchcph  18663  minveclem2  18786  ovolunlem1a  18851  ovolscalem1  18868  voliunlem1  18903  volcn  18957  itg1climres  19065  mbfi1fseqlem5  19070  mbfi1fseqlem6  19071  itg2const2  19092  itg2seq  19093  itg2mulc  19098  itg2splitlem  19099  itg2monolem1  19101  itg2i1fseqle  19105  itg2i1fseq  19106  itg2i1fseq2  19107  itg2addlem  19109  itg2cnlem1  19112  itg2cnlem2  19113  iblss  19155  itgle  19160  ibladdlem  19170  iblabs  19179  iblabsr  19180  iblmulc2  19181  itgabs  19185  bddmulibl  19189  dvfsumabs  19366  dvfsumlem2  19370  dvfsum2  19377  deg1suble  19489  deg1mul3le  19498  plyeq0lem  19588  dgrcolem2  19651  geolim3  19715  aaliou3lem2  19719  aaliou3lem8  19721  ulmdvlem1  19773  radcnvlem1  19785  radcnvlem2  19786  dvradcnv  19793  pserulm  19794  pserdvlem2  19800  abelthlem2  19804  abelthlem5  19807  abelthlem7  19810  abelth2  19814  tangtx  19869  tanabsge  19870  tanord1  19895  argregt0  19960  argrege0  19961  argimgt0  19962  logcnlem4  19988  logtayllem  20002  abscxpbnd  20089  ang180lem2  20104  atanlogsublem  20207  atans2  20223  leibpi  20234  birthdaylem3  20244  cxplim  20262  cxp2limlem  20266  cxploglim2  20269  jensenlem2  20278  jensen  20279  amgmlem  20280  emcllem2  20286  emcllem4  20288  emcllem7  20291  ftalem5  20310  basellem4  20317  basellem6  20319  basellem8  20321  basellem9  20322  chtwordi  20390  chpwordi  20391  ppiwordi  20396  ppiub  20439  vmalelog  20440  chtlepsi  20441  chtleppi  20445  chtublem  20446  chtub  20447  chpub  20455  logfaclbnd  20457  logfacrlim  20459  bcmono  20512  bclbnd  20515  bposlem1  20519  bposlem6  20524  bposlem9  20527  lgsqrlem4  20579  chebbnd1lem1  20614  chebbnd1lem3  20616  chebbnd1  20617  chtppilimlem1  20618  vmadivsum  20627  rplogsumlem2  20630  dchrisumlema  20633  dchrisumlem3  20636  dchrmusum2  20639  dchrvmasumlem3  20644  dchrvmasumiflem1  20646  dchrisum0flblem1  20653  dchrisum0re  20658  dchrisum0lem2a  20662  mulogsumlem  20676  mulog2sumlem1  20679  mulog2sumlem2  20680  2vmadivsumlem  20685  selberg2lem  20695  selberg3lem1  20702  selberg4lem1  20705  pntrlog2bndlem3  20724  pntrlog2bndlem5  20726  pntrlog2bndlem6  20728  pntpbnd1  20731  pntlemc  20740  pntlemr  20747  pntlemk  20751  pntlemo  20752  abvcxp  20760  padicabv  20775  ostth2lem2  20779  ostth2lem3  20780  ostth2lem4  20781  ostth2  20782  nvmtri  21231  imsmetlem  21253  vacn  21261  nmcvcn  21262  smcnlem  21264  blometi  21375  ipblnfi  21428  minvecolem2  21448  hhssnv  21837  nmcoplbi  22604  nmopcoi  22671  nmopcoadji  22677  idleop  22707  cdj1i  23009  zetacvg  23096  derangenlem  23109  subfaclefac  23114  subfaclim  23126  erdszelem10  23138  sinccvglem  23412  cntrset  25013  mslb1  25018  trirn  25874  mettrifi  25884  equivbnd2  25927  heiborlem6  25951  bfplem1  25957  bfp  25959  rrnmet  25964  rrndstprj1  25965  rrndstprj2  25966  irrapxlem5  26322  pell1qrge1  26366  pell1qrgaplem  26369  pell14qrgapw  26372  pellqrex  26375  pellfund14  26394  expmordi  26443  jm2.17a  26458  jm2.17c  26460  acongeq  26481  jm2.19  26497  jm2.27a  26509  jm2.27c  26511  jm3.1lem2  26522  stoweidlem3  27163  wallispilem1  27225  wallispilem5  27229  stirlinglem1  27234  stirlinglem5  27238  stirlinglem8  27241  stirlinglem10  27243  stirlinglem11  27244  dalawlem3  29341  dalawlem4  29342  dalawlem6  29344  dalawlem9  29347  dalawlem11  29349  dalawlem12  29350  dalawlem15  29353  cdleme3c  29698  cdleme7e  29715  cdleme26e  29827  cdleme26eALTN  29829  cdleme27a  29835  cdleme32c  29911  cdleme32e  29913  cdleme32le  29915  cdlemg9b  30101  cdlemg12b  30112  cdlemg12d  30114  trlcolem  30194  trlcone  30196  cdlemk7  30316  cdlemk7u  30338  cdlemk39  30384  cdlemk11ta  30397  cdlemk11tc  30413  mapdcnvatN  31135
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-rab 2553  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650  df-br 4025
  Copyright terms: Public domain W3C validator