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

Theorem 3brtr4d 5090
Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005.)
Hypotheses
Ref Expression
3brtr4d.1 (𝜑𝐴𝑅𝐵)
3brtr4d.2 (𝜑𝐶 = 𝐴)
3brtr4d.3 (𝜑𝐷 = 𝐵)
Assertion
Ref Expression
3brtr4d (𝜑𝐶𝑅𝐷)

Proof of Theorem 3brtr4d
StepHypRef Expression
1 3brtr4d.1 . 2 (𝜑𝐴𝑅𝐵)
2 3brtr4d.2 . . 3 (𝜑𝐶 = 𝐴)
3 3brtr4d.3 . . 3 (𝜑𝐷 = 𝐵)
42, 3breq12d 5071 . 2 (𝜑 → (𝐶𝑅𝐷𝐴𝑅𝐵))
51, 4mpbird 258 1 (𝜑𝐶𝑅𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528   class class class wbr 5058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5059
This theorem is referenced by:  f1oiso2  7094  sucdom2  8703  ordtypelem6  8976  fin23lem26  9736  distrnq  10372  lediv12a  11522  recp1lt1  11527  ifle  12580  xleadd1a  12636  xlemul1a  12671  fldiv4p1lem1div2  13195  fldiv4lem1div2  13197  quoremz  13213  quoremnn0ALT  13215  intfracq  13217  modmulnn  13247  fzennn  13326  monoord2  13391  expgt1  13457  expmordi  13521  leexp2r  13528  leexp1a  13529  bernneq  13580  expmulnbnd  13586  digit1  13588  faclbnd  13640  faclbnd4lem3  13645  faclbnd4lem4  13646  faclbnd6  13649  facubnd  13650  hashdomi  13731  fzsdom2  13779  absrele  14658  absimle  14659  abstri  14680  abs2difabs  14684  limsupval2  14827  rlimrege0  14926  rlimrecl  14927  climsqz  14987  climsqz2  14988  rlimdiv  14992  rlimsqz  14996  rlimsqz2  14997  isercolllem1  15011  isercoll2  15015  fsumcvg2  15074  fsumrlim  15156  o1fsum  15158  cvgcmpce  15163  isumle  15189  climcndslem1  15194  climcndslem2  15195  harmonic  15204  expcnv  15209  explecnv  15210  geomulcvg  15222  efcllem  15421  ege2le3  15433  eflegeo  15464  rpnnen2lem4  15560  ruclem2  15575  ruclem8  15580  fsumdvds  15648  phibnd  16098  iserodd  16162  pcdvdstr  16202  pcprmpw2  16208  pockthg  16232  prmreclem4  16245  prmolefac  16372  2expltfac  16416  mod2ile  17706  odsubdvds  18627  pgpfi  18661  fislw  18681  efgredlemd  18801  efgredlem  18804  frgpcpbl  18816  abvres  19541  abvtrivd  19542  znrrg  20642  cstucnd  22822  psmetge0  22851  psmetres2  22853  xmetge0  22883  xmetres2  22900  imasf1oxmet  22914  comet  23052  stdbdxmet  23054  dscmet  23111  nrmmetd  23113  nmrtri  23162  tngngp  23192  nmolb2d  23256  nmoleub  23269  nmoco  23275  nmotri  23277  nmoid  23280  nmods  23282  cnmet  23309  xrsxmet  23346  metdstri  23388  metnrmlem3  23398  lebnumlem3  23496  ipcau2  23766  tcphcphlem1  23767  tcphcph  23769  trirn  23932  rrxmet  23940  rrxdstprj1  23941  minveclem2  23958  ovolunlem1a  24026  ovolscalem1  24043  volss  24063  voliunlem1  24080  volcn  24136  itg1climres  24244  mbfi1fseqlem5  24249  mbfi1fseqlem6  24250  itg2const2  24271  itg2seq  24272  itg2mulc  24277  itg2splitlem  24278  itg2monolem1  24280  itg2i1fseqle  24284  itg2i1fseq  24285  itg2i1fseq2  24286  itg2addlem  24288  itg2cnlem1  24291  itg2cnlem2  24292  iblss  24334  itgle  24339  ibladdlem  24349  iblabs  24358  iblabsr  24359  iblmulc2  24360  itgabs  24364  bddmulibl  24368  dvfsumabs  24549  dvfsumlem2  24553  dvfsum2  24560  deg1suble  24630  deg1mul3le  24639  plyeq0lem  24729  dgrcolem2  24793  geolim3  24857  aaliou3lem2  24861  aaliou3lem8  24863  ulmdvlem1  24917  radcnvlem1  24930  radcnvlem2  24931  dvradcnv  24938  pserulm  24939  pserdvlem2  24945  abelthlem2  24949  abelthlem5  24952  abelthlem7  24955  abelth2  24959  tangtx  25020  tanabsge  25021  tanord1  25048  argregt0  25120  argrege0  25121  argimgt0  25122  abslogle  25128  logcnlem4  25155  logtayllem  25169  abscxpbnd  25261  ang180lem2  25315  atanlogsublem  25420  atans2  25436  leibpi  25448  birthdaylem3  25459  cxplim  25477  cxp2limlem  25481  cxploglim2  25484  jensenlem2  25493  jensen  25494  amgmlem  25495  emcllem2  25502  emcllem4  25504  emcllem7  25507  zetacvg  25520  lgamgulmlem2  25535  lgamgulmlem5  25538  ftalem5  25582  basellem4  25589  basellem6  25591  basellem8  25593  basellem9  25594  chtwordi  25661  chpwordi  25662  ppiwordi  25667  ppiub  25708  vmalelog  25709  chtlepsi  25710  chtleppi  25714  chtublem  25715  chtub  25716  chpub  25724  logfaclbnd  25726  logfacrlim  25728  dchrptlem3  25770  bcmono  25781  bclbnd  25784  bposlem1  25788  bposlem6  25793  bposlem9  25796  lgsqrlem4  25853  2lgslem1c  25897  chebbnd1lem1  25973  chebbnd1lem3  25975  chebbnd1  25976  chtppilimlem1  25977  vmadivsum  25986  rplogsumlem2  25989  dchrisumlema  25992  dchrisumlem3  25995  dchrmusum2  25998  dchrvmasumlem3  26003  dchrvmasumiflem1  26005  dchrisum0flblem1  26012  dchrisum0re  26017  dchrisum0lem2a  26021  mulogsumlem  26035  mulog2sumlem1  26038  mulog2sumlem2  26039  2vmadivsumlem  26044  selberg2lem  26054  selberg3lem1  26061  selberg4lem1  26064  pntrlog2bndlem3  26083  pntrlog2bndlem5  26085  pntrlog2bndlem6  26087  pntpbnd1  26090  pntlemc  26099  pntlemr  26106  pntlemk  26110  pntlemo  26111  abvcxp  26119  ostth2lem1  26122  padicabv  26134  ostth2lem2  26138  ostth2lem3  26139  ostth2lem4  26140  ostth2  26141  legso  26313  trgcopy  26518  eucrct2eupth  27952  nvmtri  28376  imsmetlem  28395  vacn  28399  nmcvcn  28400  smcnlem  28402  blometi  28508  ipblnfi  28560  minvecolem2  28580  hhssnv  28969  nmcoplbi  29733  nmopcoi  29800  nmopcoadji  29806  idleop  29836  cdj1i  30138  isoun  30364  xlt2addrd  30409  omndmul  30643  ogrpsub  30645  gsumle  30653  cycpmconjslem2  30725  archirngz  30746  ofldchr  30815  lssdimle  30906  fedgmullem2  30926  pstmxmet  31037  nexple  31168  esumpmono  31238  esumcvg  31245  meascnbl  31378  omsmon  31456  omsmeas  31481  dstfrvinc  31634  hgt750lemd  31819  hgt750lema  31828  hgt750leme  31829  swrdwlk  32271  derangenlem  32316  subfaclefac  32321  subfaclim  32333  erdszelem10  32345  sinccvglem  32813  iprodefisum  32871  noextendlt  33074  noextendgt  33075  nosupbnd1  33112  nosupbnd2lem1  33113  unbdqndv2lem2  33747  itg2gt0cn  34829  ibladdnclem  34830  iblabsnc  34838  iblmulc2nc  34839  itgabsnc  34843  bddiblnc  34844  ftc1anclem7  34855  ftc1anclem8  34856  ftc1anc  34857  mettrifi  34915  equivbnd2  34953  heiborlem6  34977  bfplem1  34983  bfp  34985  rrnmet  34990  rrndstprj1  34991  rrndstprj2  34992  dalawlem3  36891  dalawlem4  36892  dalawlem6  36894  dalawlem9  36897  dalawlem11  36899  dalawlem12  36900  dalawlem15  36903  cdleme3c  37248  cdleme7e  37265  cdleme26e  37377  cdleme26eALTN  37379  cdleme27a  37385  cdleme32c  37461  cdleme32e  37463  cdleme32le  37465  cdlemg9b  37651  cdlemg12b  37662  cdlemg12d  37664  trlcolem  37744  trlcone  37746  cdlemk7  37866  cdlemk7u  37888  cdlemk39  37934  cdlemk11ta  37947  cdlemk11tc  37963  mapdcnvatN  38684  frlmvscadiccat  39025  3cubeslem1  39161  irrapxlem5  39303  pell1qrge1  39347  pell1qrgaplem  39350  pell14qrgapw  39353  pellqrex  39356  pellfund14  39375  jm2.17a  39437  jm2.17c  39439  acongeq  39460  jm2.19  39470  jm2.27a  39482  jm2.27c  39484  jm3.1lem2  39495  areaquad  39703  rp-isfinite6  39764  hashnzfzclim  40534  binomcxplemnotnn0  40568  absimlere  41636  monoord2xrv  41640  ltmod  41799  dvbdfbdioolem2  42094  ioodvbdlimc1lem2  42097  ioodvbdlimc2lem  42099  stoweidlem3  42169  stoweidlem26  42192  wallispilem1  42231  wallispilem5  42235  stirlinglem1  42240  stirlinglem5  42244  stirlinglem8  42247  stirlinglem10  42249  stirlinglem12  42251  fourierdlem6  42279  fourierdlem7  42280  fourierdlem14  42287  fourierdlem19  42292  fourierdlem35  42308  fourierdlem39  42312  fourierdlem42  42315  fourierdlem50  42322  fourierdlem73  42345  fourierdlem76  42348  fourierdlem77  42349  fourierdlem81  42353  fourierdlem90  42362  fourierdlem92  42364  fourierdlem93  42365  fourierdlem111  42383  fouriersw  42397  etransclem38  42438  sge0split  42572  lighneallem4a  43620  rnghmsubcsetc  44146  rhmsubcsetc  44192  rhmsubcrngc  44198  rhmsubc  44259  rhmsubcALTV  44277  logbpw2m1  44525  dignn0flhalflem1  44573  dignn0flhalflem2  44574  2itscp  44666  amgmwlem  44801
  Copyright terms: Public domain W3C validator