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

Theorem 3brtr4d 5074
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 5055 . 2 (𝜑 → (𝐶𝑅𝐷𝐴𝑅𝐵))
51, 4mpbird 259 1 (𝜑𝐶𝑅𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1537   class class class wbr 5042
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-rab 3134  df-v 3475  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4270  df-if 4444  df-sn 4544  df-pr 4546  df-op 4550  df-br 5043
This theorem is referenced by:  f1oiso2  7082  sucdom2  8692  ordtypelem6  8965  fin23lem26  9725  distrnq  10361  lediv12a  11511  recp1lt1  11516  ifle  12569  xleadd1a  12625  xlemul1a  12660  fldiv4p1lem1div2  13189  fldiv4lem1div2  13191  quoremz  13207  quoremnn0ALT  13209  intfracq  13211  modmulnn  13241  fzennn  13320  monoord2  13386  expgt1  13452  expmordi  13516  leexp2r  13523  leexp1a  13524  bernneq  13575  expmulnbnd  13581  digit1  13583  faclbnd  13635  faclbnd4lem3  13640  faclbnd4lem4  13641  faclbnd6  13644  facubnd  13645  hashdomi  13726  fzsdom2  13774  absrele  14648  absimle  14649  abstri  14670  abs2difabs  14674  limsupval2  14817  rlimrege0  14916  rlimrecl  14917  climsqz  14977  climsqz2  14978  rlimdiv  14982  rlimsqz  14986  rlimsqz2  14987  isercolllem1  15001  isercoll2  15005  fsumcvg2  15064  fsumrlim  15146  o1fsum  15148  cvgcmpce  15153  isumle  15179  climcndslem1  15184  climcndslem2  15185  harmonic  15194  expcnv  15199  explecnv  15200  geomulcvg  15212  efcllem  15411  ege2le3  15423  eflegeo  15454  rpnnen2lem4  15550  ruclem2  15565  ruclem8  15570  fsumdvds  15638  phibnd  16086  iserodd  16150  pcdvdstr  16190  pcprmpw2  16196  pockthg  16220  prmreclem4  16233  prmolefac  16360  2expltfac  16405  mod2ile  17695  odsubdvds  18675  pgpfi  18709  fislw  18729  efgredlemd  18849  efgredlem  18852  frgpcpbl  18864  abvres  19586  abvtrivd  19587  znrrg  20688  cstucnd  22869  psmetge0  22898  psmetres2  22900  xmetge0  22930  xmetres2  22947  imasf1oxmet  22961  comet  23099  stdbdxmet  23101  dscmet  23158  nrmmetd  23160  nmrtri  23209  tngngp  23239  nmolb2d  23303  nmoleub  23316  nmoco  23322  nmotri  23324  nmoid  23327  nmods  23329  cnmet  23356  xrsxmet  23393  metdstri  23435  metnrmlem3  23445  lebnumlem3  23547  ipcau2  23817  tcphcphlem1  23818  tcphcph  23820  trirn  23983  rrxmet  23991  rrxdstprj1  23992  minveclem2  24009  ovolunlem1a  24079  ovolscalem1  24096  volss  24116  voliunlem1  24133  volcn  24189  itg1climres  24297  mbfi1fseqlem5  24302  mbfi1fseqlem6  24303  itg2const2  24324  itg2seq  24325  itg2mulc  24330  itg2splitlem  24331  itg2monolem1  24333  itg2i1fseqle  24337  itg2i1fseq  24338  itg2i1fseq2  24339  itg2addlem  24341  itg2cnlem1  24344  itg2cnlem2  24345  iblss  24387  itgle  24392  ibladdlem  24402  iblabs  24411  iblabsr  24412  iblmulc2  24413  itgabs  24417  bddmulibl  24421  bddiblnc  24424  dvfsumabs  24605  dvfsumlem2  24609  dvfsum2  24616  deg1suble  24687  deg1mul3le  24696  plyeq0lem  24786  dgrcolem2  24850  geolim3  24914  aaliou3lem2  24918  aaliou3lem8  24920  ulmdvlem1  24974  radcnvlem1  24987  radcnvlem2  24988  dvradcnv  24995  pserulm  24996  pserdvlem2  25002  abelthlem2  25006  abelthlem5  25009  abelthlem7  25012  abelth2  25016  tangtx  25077  tanabsge  25078  tanord1  25108  argregt0  25180  argrege0  25181  argimgt0  25182  abslogle  25188  logcnlem4  25215  logtayllem  25229  abscxpbnd  25321  ang180lem2  25375  atanlogsublem  25480  atans2  25496  leibpi  25507  birthdaylem3  25518  cxplim  25536  cxp2limlem  25540  cxploglim2  25543  jensenlem2  25552  jensen  25553  amgmlem  25554  emcllem2  25561  emcllem4  25563  emcllem7  25566  zetacvg  25579  lgamgulmlem2  25594  lgamgulmlem5  25597  ftalem5  25641  basellem4  25648  basellem6  25650  basellem8  25652  basellem9  25653  chtwordi  25720  chpwordi  25721  ppiwordi  25726  ppiub  25767  vmalelog  25768  chtlepsi  25769  chtleppi  25773  chtublem  25774  chtub  25775  chpub  25783  logfaclbnd  25785  logfacrlim  25787  dchrptlem3  25829  bcmono  25840  bclbnd  25843  bposlem1  25847  bposlem6  25852  bposlem9  25855  lgsqrlem4  25912  2lgslem1c  25956  chebbnd1lem1  26032  chebbnd1lem3  26034  chebbnd1  26035  chtppilimlem1  26036  vmadivsum  26045  rplogsumlem2  26048  dchrisumlema  26051  dchrisumlem3  26054  dchrmusum2  26057  dchrvmasumlem3  26062  dchrvmasumiflem1  26064  dchrisum0flblem1  26071  dchrisum0re  26076  dchrisum0lem2a  26080  mulogsumlem  26094  mulog2sumlem1  26097  mulog2sumlem2  26098  2vmadivsumlem  26103  selberg2lem  26113  selberg3lem1  26120  selberg4lem1  26123  pntrlog2bndlem3  26142  pntrlog2bndlem5  26144  pntrlog2bndlem6  26146  pntpbnd1  26149  pntlemc  26158  pntlemr  26165  pntlemk  26169  pntlemo  26170  abvcxp  26178  ostth2lem1  26181  padicabv  26193  ostth2lem2  26197  ostth2lem3  26198  ostth2lem4  26199  ostth2  26200  legso  26372  trgcopy  26577  eucrct2eupth  28009  nvmtri  28433  imsmetlem  28452  vacn  28456  nmcvcn  28457  smcnlem  28459  blometi  28565  ipblnfi  28617  minvecolem2  28637  hhssnv  29026  nmcoplbi  29790  nmopcoi  29857  nmopcoadji  29863  idleop  29893  cdj1i  30195  isoun  30424  xlt2addrd  30469  omndmul  30723  ogrpsub  30725  gsumle  30733  cycpmconjslem2  30805  archirngz  30826  ofldchr  30895  lssdimle  31017  fedgmullem2  31037  pstmxmet  31148  nexple  31276  esumpmono  31346  esumcvg  31353  meascnbl  31486  omsmon  31564  omsmeas  31589  dstfrvinc  31742  hgt750lemd  31927  hgt750lema  31936  hgt750leme  31937  swrdwlk  32381  derangenlem  32426  subfaclefac  32431  subfaclim  32443  erdszelem10  32455  sinccvglem  32923  iprodefisum  32981  noextendlt  33184  noextendgt  33185  nosupbnd1  33222  nosupbnd2lem1  33223  unbdqndv2lem2  33857  itg2gt0cn  34988  ibladdnclem  34989  iblabsnc  34997  iblmulc2nc  34998  itgabsnc  35002  ftc1anclem7  35012  ftc1anclem8  35013  ftc1anc  35014  mettrifi  35071  equivbnd2  35106  heiborlem6  35130  bfplem1  35136  bfp  35138  rrnmet  35143  rrndstprj1  35144  rrndstprj2  35145  dalawlem3  37045  dalawlem4  37046  dalawlem6  37048  dalawlem9  37051  dalawlem11  37053  dalawlem12  37054  dalawlem15  37057  cdleme3c  37402  cdleme7e  37419  cdleme26e  37531  cdleme26eALTN  37533  cdleme27a  37539  cdleme32c  37615  cdleme32e  37617  cdleme32le  37619  cdlemg9b  37805  cdlemg12b  37816  cdlemg12d  37818  trlcolem  37898  trlcone  37900  cdlemk7  38020  cdlemk7u  38042  cdlemk39  38088  cdlemk11ta  38101  cdlemk11tc  38117  mapdcnvatN  38838  factwoffsmonot  39210  frlmvscadiccat  39257  3cubeslem1  39418  irrapxlem5  39560  pell1qrge1  39604  pell1qrgaplem  39607  pell14qrgapw  39610  pellqrex  39613  pellfund14  39632  jm2.17a  39694  jm2.17c  39696  acongeq  39717  jm2.19  39727  jm2.27a  39739  jm2.27c  39741  jm3.1lem2  39752  areaquad  39959  rp-isfinite6  40019  hashnzfzclim  40809  binomcxplemnotnn0  40843  absimlere  41910  monoord2xrv  41914  ltmod  42071  dvbdfbdioolem2  42362  ioodvbdlimc1lem2  42365  ioodvbdlimc2lem  42367  stoweidlem3  42436  stoweidlem26  42459  wallispilem1  42498  wallispilem5  42502  stirlinglem1  42507  stirlinglem5  42511  stirlinglem8  42514  stirlinglem10  42516  stirlinglem12  42518  fourierdlem6  42546  fourierdlem7  42547  fourierdlem14  42554  fourierdlem19  42559  fourierdlem35  42575  fourierdlem39  42579  fourierdlem42  42582  fourierdlem50  42589  fourierdlem73  42612  fourierdlem76  42615  fourierdlem77  42616  fourierdlem81  42620  fourierdlem90  42629  fourierdlem92  42631  fourierdlem93  42632  fourierdlem111  42650  fouriersw  42664  etransclem38  42705  sge0split  42839  lighneallem4a  43918  rnghmsubcsetc  44393  rhmsubcsetc  44439  rhmsubcrngc  44445  rhmsubc  44506  rhmsubcALTV  44524  logbpw2m1  44772  dignn0flhalflem1  44820  dignn0flhalflem2  44821  2itscp  44955  amgmwlem  45090
  Copyright terms: Public domain W3C validator