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

Theorem 3brtr4d 4055
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 4038 . 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 1625   class class class wbr 4025
This theorem is referenced by:  f1oiso2  5851  sucdom2  7059  ordtypelem6  7240  cdaen  7801  cdacomen  7809  cdadom1  7814  fin23lem26  7953  distrnq  8587  lediv12a  9651  recp1lt1  9656  ifle  10526  xleadd1a  10575  xlemul1a  10610  quoremz  10961  quoremnn0ALT  10963  intfracq  10965  modmulnn  10990  fzennn  11032  monoord2  11079  expgt1  11142  leexp2r  11161  leexp1a  11162  bernneq  11229  expmulnbnd  11235  digit1  11237  faclbnd  11305  faclbnd4lem3  11310  faclbnd4lem4  11311  faclbnd6  11314  facubnd  11315  hashdomi  11364  fzsdom2  11384  absrele  11795  absimle  11796  abstri  11816  abs2difabs  11820  limsupval2  11956  rlimrege0  12055  rlimrecl  12056  climsqz  12116  climsqz2  12117  rlimdiv  12121  rlimsqz  12125  rlimsqz2  12126  isercolllem1  12140  isercoll2  12144  fsumcvg2  12202  fsumrlim  12271  o1fsum  12273  cvgcmpce  12278  isumle  12305  climcndslem1  12310  climcndslem2  12311  harmonic  12319  expcnv  12324  explecnv  12325  geomulcvg  12334  efcllem  12361  ege2le3  12373  eflegeo  12403  rpnnen2lem4  12498  ruclem2  12512  ruclem8  12517  fsumdvds  12574  phibnd  12841  iserodd  12890  pcdvdstr  12930  pcprmpw2  12936  pockthg  12955  prmreclem4  12968  2expltfac  13107  mod2ile  14214  odsubdvds  14884  pgpfi  14918  fislw  14938  efgredlemd  15055  efgredlem  15058  frgpcpbl  15070  abvres  15606  abvtrivd  15607  znrrg  16521  xmetge0  17911  xmetres2  17927  imasf1oxmet  17941  comet  18061  stdbdxmet  18063  dscmet  18097  nrmmetd  18099  nmrtri  18147  tngngp  18172  nmolb2d  18229  nmoleub  18242  nmoco  18248  nmotri  18250  nmoid  18253  nmods  18255  cnmet  18283  xrsxmet  18317  metdstri  18357  metnrmlem3  18367  lebnumlem3  18463  ipcau2  18666  tchcphlem1  18667  tchcph  18669  minveclem2  18792  ovolunlem1a  18857  ovolscalem1  18874  voliunlem1  18909  volcn  18963  itg1climres  19071  mbfi1fseqlem5  19076  mbfi1fseqlem6  19077  itg2const2  19098  itg2seq  19099  itg2mulc  19104  itg2splitlem  19105  itg2monolem1  19107  itg2i1fseqle  19111  itg2i1fseq  19112  itg2i1fseq2  19113  itg2addlem  19115  itg2cnlem1  19118  itg2cnlem2  19119  iblss  19161  itgle  19166  ibladdlem  19176  iblabs  19185  iblabsr  19186  iblmulc2  19187  itgabs  19191  bddmulibl  19195  dvfsumabs  19372  dvfsumlem2  19376  dvfsum2  19383  deg1suble  19495  deg1mul3le  19504  plyeq0lem  19594  dgrcolem2  19657  geolim3  19721  aaliou3lem2  19725  aaliou3lem8  19727  ulmdvlem1  19779  radcnvlem1  19791  radcnvlem2  19792  dvradcnv  19799  pserulm  19800  pserdvlem2  19806  abelthlem2  19810  abelthlem5  19813  abelthlem7  19816  abelth2  19820  tangtx  19875  tanabsge  19876  tanord1  19901  argregt0  19966  argrege0  19967  argimgt0  19968  logcnlem4  19994  logtayllem  20008  abscxpbnd  20095  ang180lem2  20110  atanlogsublem  20213  atans2  20229  leibpi  20240  birthdaylem3  20250  cxplim  20268  cxp2limlem  20272  cxploglim2  20275  jensenlem2  20284  jensen  20285  amgmlem  20286  emcllem2  20292  emcllem4  20294  emcllem7  20297  ftalem5  20316  basellem4  20323  basellem6  20325  basellem8  20327  basellem9  20328  chtwordi  20396  chpwordi  20397  ppiwordi  20402  ppiub  20445  vmalelog  20446  chtlepsi  20447  chtleppi  20451  chtublem  20452  chtub  20453  chpub  20461  logfaclbnd  20463  logfacrlim  20465  bcmono  20518  bclbnd  20521  bposlem1  20525  bposlem6  20530  bposlem9  20533  lgsqrlem4  20585  chebbnd1lem1  20620  chebbnd1lem3  20622  chebbnd1  20623  chtppilimlem1  20624  vmadivsum  20633  rplogsumlem2  20636  dchrisumlema  20639  dchrisumlem3  20642  dchrmusum2  20645  dchrvmasumlem3  20650  dchrvmasumiflem1  20652  dchrisum0flblem1  20659  dchrisum0re  20664  dchrisum0lem2a  20668  mulogsumlem  20682  mulog2sumlem1  20685  mulog2sumlem2  20686  2vmadivsumlem  20691  selberg2lem  20701  selberg3lem1  20708  selberg4lem1  20711  pntrlog2bndlem3  20730  pntrlog2bndlem5  20732  pntrlog2bndlem6  20734  pntpbnd1  20737  pntlemc  20746  pntlemr  20753  pntlemk  20757  pntlemo  20758  abvcxp  20766  padicabv  20781  ostth2lem2  20785  ostth2lem3  20786  ostth2lem4  20787  ostth2  20788  nvmtri  21239  imsmetlem  21261  vacn  21269  nmcvcn  21270  smcnlem  21272  blometi  21383  ipblnfi  21436  minvecolem2  21456  hhssnv  21843  nmcoplbi  22610  nmopcoi  22677  nmopcoadji  22683  idleop  22713  cdj1i  23015  esumpmono  23449  esumcvg  23456  dstfrvinc  23679  zetacvg  23691  derangenlem  23704  subfaclefac  23709  subfaclim  23721  erdszelem10  23733  sinccvglem  24007  cntrset  25613  mslb1  25618  trirn  26474  mettrifi  26484  equivbnd2  26527  heiborlem6  26551  bfplem1  26557  bfp  26559  rrnmet  26564  rrndstprj1  26565  rrndstprj2  26566  irrapxlem5  26922  pell1qrge1  26966  pell1qrgaplem  26969  pell14qrgapw  26972  pellqrex  26975  pellfund14  26994  expmordi  27043  jm2.17a  27058  jm2.17c  27060  acongeq  27081  jm2.19  27097  jm2.27a  27109  jm2.27c  27111  jm3.1lem2  27122  stoweidlem3  27763  wallispilem1  27825  wallispilem5  27829  stirlinglem1  27834  stirlinglem5  27838  stirlinglem8  27841  stirlinglem10  27843  stirlinglem11  27844  dalawlem3  30135  dalawlem4  30136  dalawlem6  30138  dalawlem9  30141  dalawlem11  30143  dalawlem12  30144  dalawlem15  30147  cdleme3c  30492  cdleme7e  30509  cdleme26e  30621  cdleme26eALTN  30623  cdleme27a  30629  cdleme32c  30705  cdleme32e  30707  cdleme32le  30709  cdlemg9b  30895  cdlemg12b  30906  cdlemg12d  30908  trlcolem  30988  trlcone  30990  cdlemk7  31110  cdlemk7u  31132  cdlemk39  31178  cdlemk11ta  31191  cdlemk11tc  31207  mapdcnvatN  31929
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-br 4026
  Copyright terms: Public domain W3C validator