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

Theorem 3brtr4d 4183
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 4166 . 2  |-  ( ph  ->  ( C R D  <-> 
A R B ) )
51, 4mpbird 224 1  |-  ( ph  ->  C R D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   class class class wbr 4153
This theorem is referenced by:  f1oiso2  6011  sucdom2  7239  ordtypelem6  7425  cdaen  7986  cdacomen  7994  cdadom1  7999  fin23lem26  8138  distrnq  8771  lediv12a  9835  recp1lt1  9840  ifle  10715  xleadd1a  10764  xlemul1a  10799  quoremz  11163  quoremnn0ALT  11165  intfracq  11167  modmulnn  11192  fzennn  11234  monoord2  11281  expgt1  11345  leexp2r  11364  leexp1a  11365  bernneq  11432  expmulnbnd  11438  digit1  11440  faclbnd  11508  faclbnd4lem3  11513  faclbnd4lem4  11514  faclbnd6  11517  facubnd  11518  hashdomi  11581  fzsdom2  11620  absrele  12040  absimle  12041  abstri  12061  abs2difabs  12065  limsupval2  12201  rlimrege0  12300  rlimrecl  12301  climsqz  12361  climsqz2  12362  rlimdiv  12366  rlimsqz  12370  rlimsqz2  12371  isercolllem1  12385  isercoll2  12389  fsumcvg2  12448  fsumrlim  12517  o1fsum  12519  cvgcmpce  12524  isumle  12551  climcndslem1  12556  climcndslem2  12557  harmonic  12565  expcnv  12570  explecnv  12571  geomulcvg  12580  efcllem  12607  ege2le3  12619  eflegeo  12649  rpnnen2lem4  12744  ruclem2  12758  ruclem8  12763  fsumdvds  12820  phibnd  13087  iserodd  13136  pcdvdstr  13176  pcprmpw2  13182  pockthg  13201  prmreclem4  13214  2expltfac  13353  mod2ile  14462  odsubdvds  15132  pgpfi  15166  fislw  15186  efgredlemd  15303  efgredlem  15306  frgpcpbl  15318  abvres  15854  abvtrivd  15855  znrrg  16769  cstucnd  18235  xmetge0  18283  xmetres2  18299  imasf1oxmet  18313  comet  18433  stdbdxmet  18435  dscmet  18491  nrmmetd  18493  nmrtri  18541  tngngp  18566  nmolb2d  18623  nmoleub  18636  nmoco  18642  nmotri  18644  nmoid  18647  nmods  18649  cnmet  18677  xrsxmet  18711  metdstri  18752  metnrmlem3  18762  lebnumlem3  18859  ipcau2  19062  tchcphlem1  19063  tchcph  19065  minveclem2  19194  ovolunlem1a  19259  ovolscalem1  19276  voliunlem1  19311  volcn  19365  itg1climres  19473  mbfi1fseqlem5  19478  mbfi1fseqlem6  19479  itg2const2  19500  itg2seq  19501  itg2mulc  19506  itg2splitlem  19507  itg2monolem1  19509  itg2i1fseqle  19513  itg2i1fseq  19514  itg2i1fseq2  19515  itg2addlem  19517  itg2cnlem1  19520  itg2cnlem2  19521  iblss  19563  itgle  19568  ibladdlem  19578  iblabs  19587  iblabsr  19588  iblmulc2  19589  itgabs  19593  bddmulibl  19597  dvfsumabs  19774  dvfsumlem2  19778  dvfsum2  19785  deg1suble  19897  deg1mul3le  19906  plyeq0lem  19996  dgrcolem2  20059  geolim3  20123  aaliou3lem2  20127  aaliou3lem8  20129  ulmdvlem1  20183  radcnvlem1  20196  radcnvlem2  20197  dvradcnv  20204  pserulm  20205  pserdvlem2  20211  abelthlem2  20215  abelthlem5  20218  abelthlem7  20221  abelth2  20225  tangtx  20280  tanabsge  20281  tanord1  20306  argregt0  20372  argrege0  20373  argimgt0  20374  abslogle  20380  logcnlem4  20403  logtayllem  20417  abscxpbnd  20504  ang180lem2  20519  atanlogsublem  20622  atans2  20638  leibpi  20649  birthdaylem3  20659  cxplim  20677  cxp2limlem  20681  cxploglim2  20684  jensenlem2  20693  jensen  20694  amgmlem  20695  emcllem2  20702  emcllem4  20704  emcllem7  20707  ftalem5  20726  basellem4  20733  basellem6  20735  basellem8  20737  basellem9  20738  chtwordi  20806  chpwordi  20807  ppiwordi  20812  ppiub  20855  vmalelog  20856  chtlepsi  20857  chtleppi  20861  chtublem  20862  chtub  20863  chpub  20871  logfaclbnd  20873  logfacrlim  20875  bcmono  20928  bclbnd  20931  bposlem1  20935  bposlem6  20940  bposlem9  20943  lgsqrlem4  20995  chebbnd1lem1  21030  chebbnd1lem3  21032  chebbnd1  21033  chtppilimlem1  21034  vmadivsum  21043  rplogsumlem2  21046  dchrisumlema  21049  dchrisumlem3  21052  dchrmusum2  21055  dchrvmasumlem3  21060  dchrvmasumiflem1  21062  dchrisum0flblem1  21069  dchrisum0re  21074  dchrisum0lem2a  21078  mulogsumlem  21092  mulog2sumlem1  21095  mulog2sumlem2  21096  2vmadivsumlem  21101  selberg2lem  21111  selberg3lem1  21118  selberg4lem1  21121  pntrlog2bndlem3  21140  pntrlog2bndlem5  21142  pntrlog2bndlem6  21144  pntpbnd1  21147  pntlemc  21156  pntlemr  21163  pntlemk  21167  pntlemo  21168  abvcxp  21176  padicabv  21191  ostth2lem2  21195  ostth2lem3  21196  ostth2lem4  21197  ostth2  21198  nvmtri  22008  imsmetlem  22030  vacn  22038  nmcvcn  22039  smcnlem  22041  blometi  22152  ipblnfi  22205  minvecolem2  22225  hhssnv  22612  nmcoplbi  23379  nmopcoi  23446  nmopcoadji  23452  idleop  23482  cdj1i  23784  isoun  23930  xlt2addrd  23960  ofldchr  24070  esumpmono  24265  esumcvg  24272  meascnbl  24367  volss  24377  dstfrvinc  24513  zetacvg  24578  lgamgulmlem2  24593  lgamgulmlem5  24596  lgamcvg2  24618  derangenlem  24636  subfaclefac  24641  subfaclim  24653  erdszelem10  24665  sinccvglem  24888  itg2gt0cn  25960  ibladdnclem  25961  iblabsnc  25969  iblmulc2nc  25970  itgabsnc  25974  bddiblnc  25975  trirn  26148  mettrifi  26154  equivbnd2  26192  heiborlem6  26216  bfplem1  26222  bfp  26224  rrnmet  26229  rrndstprj1  26230  rrndstprj2  26231  irrapxlem5  26580  pell1qrge1  26624  pell1qrgaplem  26627  pell14qrgapw  26630  pellqrex  26633  pellfund14  26652  expmordi  26701  jm2.17a  26716  jm2.17c  26718  acongeq  26739  jm2.19  26755  jm2.27a  26767  jm2.27c  26769  jm3.1lem2  26780  stoweidlem3  27420  stoweidlem26  27443  wallispilem1  27482  wallispilem5  27486  stirlinglem1  27491  stirlinglem5  27495  stirlinglem8  27498  stirlinglem10  27500  stirlinglem12  27502  dalawlem3  29987  dalawlem4  29988  dalawlem6  29990  dalawlem9  29993  dalawlem11  29995  dalawlem12  29996  dalawlem15  29999  cdleme3c  30344  cdleme7e  30361  cdleme26e  30473  cdleme26eALTN  30475  cdleme27a  30481  cdleme32c  30557  cdleme32e  30559  cdleme32le  30561  cdlemg9b  30747  cdlemg12b  30758  cdlemg12d  30760  trlcolem  30840  trlcone  30842  cdlemk7  30962  cdlemk7u  30984  cdlemk39  31030  cdlemk11ta  31043  cdlemk11tc  31059  mapdcnvatN  31781
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
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 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-br 4154
  Copyright terms: Public domain W3C validator