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

Theorem 3brtr4d 4053
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 4036 . 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 4023
This theorem is referenced by:  f1oiso2  5849  sucdom2  7057  ordtypelem6  7238  cdaen  7799  cdacomen  7807  cdadom1  7812  fin23lem26  7951  distrnq  8585  lediv12a  9649  recp1lt1  9654  ifle  10524  xleadd1a  10573  xlemul1a  10608  quoremz  10959  quoremnn0ALT  10961  intfracq  10963  modmulnn  10988  fzennn  11030  monoord2  11077  expgt1  11140  leexp2r  11159  leexp1a  11160  bernneq  11227  expmulnbnd  11233  digit1  11235  faclbnd  11303  faclbnd4lem3  11308  faclbnd4lem4  11309  faclbnd6  11312  facubnd  11313  hashdomi  11362  fzsdom2  11382  absrele  11793  absimle  11794  abstri  11814  abs2difabs  11818  limsupval2  11954  rlimrege0  12053  rlimrecl  12054  climsqz  12114  climsqz2  12115  rlimdiv  12119  rlimsqz  12123  rlimsqz2  12124  isercolllem1  12138  isercoll2  12142  fsumcvg2  12200  fsumrlim  12269  o1fsum  12271  cvgcmpce  12276  isumle  12303  climcndslem1  12308  climcndslem2  12309  harmonic  12317  expcnv  12322  explecnv  12323  geomulcvg  12332  efcllem  12359  ege2le3  12371  eflegeo  12401  rpnnen2lem4  12496  ruclem2  12510  ruclem8  12515  fsumdvds  12572  phibnd  12839  iserodd  12888  pcdvdstr  12928  pcprmpw2  12934  pockthg  12953  prmreclem4  12966  2expltfac  13105  mod2ile  14212  odsubdvds  14882  pgpfi  14916  fislw  14936  efgredlemd  15053  efgredlem  15056  frgpcpbl  15068  abvres  15604  abvtrivd  15605  znrrg  16519  xmetge0  17909  xmetres2  17925  imasf1oxmet  17939  comet  18059  stdbdxmet  18061  dscmet  18095  nrmmetd  18097  nmrtri  18145  tngngp  18170  nmolb2d  18227  nmoleub  18240  nmoco  18246  nmotri  18248  nmoid  18251  nmods  18253  cnmet  18281  xrsxmet  18315  metdstri  18355  metnrmlem3  18365  lebnumlem3  18461  ipcau2  18664  tchcphlem1  18665  tchcph  18667  minveclem2  18790  ovolunlem1a  18855  ovolscalem1  18872  voliunlem1  18907  volcn  18961  itg1climres  19069  mbfi1fseqlem5  19074  mbfi1fseqlem6  19075  itg2const2  19096  itg2seq  19097  itg2mulc  19102  itg2splitlem  19103  itg2monolem1  19105  itg2i1fseqle  19109  itg2i1fseq  19110  itg2i1fseq2  19111  itg2addlem  19113  itg2cnlem1  19116  itg2cnlem2  19117  iblss  19159  itgle  19164  ibladdlem  19174  iblabs  19183  iblabsr  19184  iblmulc2  19185  itgabs  19189  bddmulibl  19193  dvfsumabs  19370  dvfsumlem2  19374  dvfsum2  19381  deg1suble  19493  deg1mul3le  19502  plyeq0lem  19592  dgrcolem2  19655  geolim3  19719  aaliou3lem2  19723  aaliou3lem8  19725  ulmdvlem1  19777  radcnvlem1  19789  radcnvlem2  19790  dvradcnv  19797  pserulm  19798  pserdvlem2  19804  abelthlem2  19808  abelthlem5  19811  abelthlem7  19814  abelth2  19818  tangtx  19873  tanabsge  19874  tanord1  19899  argregt0  19964  argrege0  19965  argimgt0  19966  logcnlem4  19992  logtayllem  20006  abscxpbnd  20093  ang180lem2  20108  atanlogsublem  20211  atans2  20227  leibpi  20238  birthdaylem3  20248  cxplim  20266  cxp2limlem  20270  cxploglim2  20273  jensenlem2  20282  jensen  20283  amgmlem  20284  emcllem2  20290  emcllem4  20292  emcllem7  20295  ftalem5  20314  basellem4  20321  basellem6  20323  basellem8  20325  basellem9  20326  chtwordi  20394  chpwordi  20395  ppiwordi  20400  ppiub  20443  vmalelog  20444  chtlepsi  20445  chtleppi  20449  chtublem  20450  chtub  20451  chpub  20459  logfaclbnd  20461  logfacrlim  20463  bcmono  20516  bclbnd  20519  bposlem1  20523  bposlem6  20528  bposlem9  20531  lgsqrlem4  20583  chebbnd1lem1  20618  chebbnd1lem3  20620  chebbnd1  20621  chtppilimlem1  20622  vmadivsum  20631  rplogsumlem2  20634  dchrisumlema  20637  dchrisumlem3  20640  dchrmusum2  20643  dchrvmasumlem3  20648  dchrvmasumiflem1  20650  dchrisum0flblem1  20657  dchrisum0re  20662  dchrisum0lem2a  20666  mulogsumlem  20680  mulog2sumlem1  20683  mulog2sumlem2  20684  2vmadivsumlem  20689  selberg2lem  20699  selberg3lem1  20706  selberg4lem1  20709  pntrlog2bndlem3  20728  pntrlog2bndlem5  20730  pntrlog2bndlem6  20732  pntpbnd1  20735  pntlemc  20744  pntlemr  20751  pntlemk  20755  pntlemo  20756  abvcxp  20764  padicabv  20779  ostth2lem2  20783  ostth2lem3  20784  ostth2lem4  20785  ostth2  20786  nvmtri  21237  imsmetlem  21259  vacn  21267  nmcvcn  21268  smcnlem  21270  blometi  21381  ipblnfi  21434  minvecolem2  21454  hhssnv  21841  nmcoplbi  22608  nmopcoi  22675  nmopcoadji  22681  idleop  22711  cdj1i  23013  esumpmono  23447  esumcvg  23454  dstfrvinc  23677  zetacvg  23689  derangenlem  23702  subfaclefac  23707  subfaclim  23719  erdszelem10  23731  sinccvglem  24005  cntrset  25602  mslb1  25607  trirn  26463  mettrifi  26473  equivbnd2  26516  heiborlem6  26540  bfplem1  26546  bfp  26548  rrnmet  26553  rrndstprj1  26554  rrndstprj2  26555  irrapxlem5  26911  pell1qrge1  26955  pell1qrgaplem  26958  pell14qrgapw  26961  pellqrex  26964  pellfund14  26983  expmordi  27032  jm2.17a  27047  jm2.17c  27049  acongeq  27070  jm2.19  27086  jm2.27a  27098  jm2.27c  27100  jm3.1lem2  27111  stoweidlem3  27752  wallispilem1  27814  wallispilem5  27818  stirlinglem1  27823  stirlinglem5  27827  stirlinglem8  27830  stirlinglem10  27832  stirlinglem11  27833  dalawlem3  30062  dalawlem4  30063  dalawlem6  30065  dalawlem9  30068  dalawlem11  30070  dalawlem12  30071  dalawlem15  30074  cdleme3c  30419  cdleme7e  30436  cdleme26e  30548  cdleme26eALTN  30550  cdleme27a  30556  cdleme32c  30632  cdleme32e  30634  cdleme32le  30636  cdlemg9b  30822  cdlemg12b  30833  cdlemg12d  30835  trlcolem  30915  trlcone  30917  cdlemk7  31037  cdlemk7u  31059  cdlemk39  31105  cdlemk11ta  31118  cdlemk11tc  31134  mapdcnvatN  31856
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 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
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 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024
  Copyright terms: Public domain W3C validator