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

Theorem 3brtr4d 4609
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 4590 . 2 (𝜑 → (𝐶𝑅𝐷𝐴𝑅𝐵))
51, 4mpbird 245 1 (𝜑𝐶𝑅𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474   class class class wbr 4577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578
This theorem is referenced by:  f1oiso2  6480  sucdom2  8019  ordtypelem6  8289  cdaen  8856  cdacomen  8864  cdadom1  8869  fin23lem26  9008  distrnq  9640  lediv12a  10768  recp1lt1  10773  ifle  11864  xleadd1a  11915  xlemul1a  11950  fldiv4p1lem1div2  12456  fldiv4lem1div2  12458  quoremz  12474  quoremnn0ALT  12476  intfracq  12478  modmulnn  12508  fzennn  12587  monoord2  12652  expgt1  12718  leexp2r  12738  leexp1a  12739  bernneq  12810  expmulnbnd  12816  digit1  12818  faclbnd  12897  faclbnd4lem3  12902  faclbnd4lem4  12903  faclbnd6  12906  facubnd  12907  hashdomi  12985  fzsdom2  13030  absrele  13845  absimle  13846  abstri  13867  abs2difabs  13871  limsupval2  14008  rlimrege0  14107  rlimrecl  14108  climsqz  14168  climsqz2  14169  rlimdiv  14173  rlimsqz  14177  rlimsqz2  14178  isercolllem1  14192  isercoll2  14196  fsumcvg2  14254  fsumrlim  14333  o1fsum  14335  cvgcmpce  14340  isumle  14364  climcndslem1  14369  climcndslem2  14370  harmonic  14379  expcnv  14384  explecnv  14385  geomulcvg  14395  efcllem  14596  ege2le3  14608  eflegeo  14639  rpnnen2lem4  14734  ruclem2  14749  ruclem8  14754  fsumdvds  14817  phibnd  15263  iserodd  15327  pcdvdstr  15367  pcprmpw2  15373  pockthg  15397  prmreclem4  15410  prmolefac  15537  2expltfac  15586  mod2ile  16878  odsubdvds  17758  pgpfi  17792  fislw  17812  efgredlemd  17929  efgredlem  17932  frgpcpbl  17944  abvres  18611  abvtrivd  18612  znrrg  19681  cstucnd  21846  psmetge0  21875  psmetres2  21877  xmetge0  21907  xmetres2  21924  imasf1oxmet  21938  comet  22076  stdbdxmet  22078  dscmet  22135  nrmmetd  22137  nmrtri  22186  tngngp  22216  nmolb2d  22280  nmoleub  22293  nmoco  22299  nmotri  22301  nmoid  22304  nmods  22306  cnmet  22333  xrsxmet  22368  metdstri  22410  metnrmlem3  22420  lebnumlem3  22518  ipcau2  22786  tchcphlem1  22787  tchcph  22789  trirn  22936  rrxmet  22944  rrxdstprj1  22945  minveclem2  22950  ovolunlem1a  23016  ovolscalem1  23033  volss  23053  voliunlem1  23070  volcn  23125  itg1climres  23232  mbfi1fseqlem5  23237  mbfi1fseqlem6  23238  itg2const2  23259  itg2seq  23260  itg2mulc  23265  itg2splitlem  23266  itg2monolem1  23268  itg2i1fseqle  23272  itg2i1fseq  23273  itg2i1fseq2  23274  itg2addlem  23276  itg2cnlem1  23279  itg2cnlem2  23280  iblss  23322  itgle  23327  ibladdlem  23337  iblabs  23346  iblabsr  23347  iblmulc2  23348  itgabs  23352  bddmulibl  23356  dvfsumabs  23535  dvfsumlem2  23539  dvfsum2  23546  deg1suble  23616  deg1mul3le  23625  plyeq0lem  23715  dgrcolem2  23779  geolim3  23843  aaliou3lem2  23847  aaliou3lem8  23849  ulmdvlem1  23903  radcnvlem1  23916  radcnvlem2  23917  dvradcnv  23924  pserulm  23925  pserdvlem2  23931  abelthlem2  23935  abelthlem5  23938  abelthlem7  23941  abelth2  23945  tangtx  24006  tanabsge  24007  tanord1  24032  argregt0  24105  argrege0  24106  argimgt0  24107  abslogle  24113  logcnlem4  24136  logtayllem  24150  abscxpbnd  24239  ang180lem2  24285  atanlogsublem  24387  atans2  24403  leibpi  24414  birthdaylem3  24425  cxplim  24443  cxp2limlem  24447  cxploglim2  24450  jensenlem2  24459  jensen  24460  amgmlem  24461  emcllem2  24468  emcllem4  24470  emcllem7  24473  zetacvg  24486  lgamgulmlem2  24501  lgamgulmlem5  24504  lgamcvg2  24526  ftalem5  24548  basellem4  24555  basellem6  24557  basellem8  24559  basellem9  24560  chtwordi  24627  chpwordi  24628  ppiwordi  24633  ppiub  24674  vmalelog  24675  chtlepsi  24676  chtleppi  24680  chtublem  24681  chtub  24682  chpub  24690  logfaclbnd  24692  logfacrlim  24694  dchrptlem3  24736  bcmono  24747  bclbnd  24750  bposlem1  24754  bposlem6  24759  bposlem9  24762  lgsqrlem4  24819  2lgslem1c  24863  chebbnd1lem1  24903  chebbnd1lem3  24905  chebbnd1  24906  chtppilimlem1  24907  vmadivsum  24916  rplogsumlem2  24919  dchrisumlema  24922  dchrisumlem3  24925  dchrmusum2  24928  dchrvmasumlem3  24933  dchrvmasumiflem1  24935  dchrisum0flblem1  24942  dchrisum0re  24947  dchrisum0lem2a  24951  mulogsumlem  24965  mulog2sumlem1  24968  mulog2sumlem2  24969  2vmadivsumlem  24974  selberg2lem  24984  selberg3lem1  24991  selberg4lem1  24994  pntrlog2bndlem3  25013  pntrlog2bndlem5  25015  pntrlog2bndlem6  25017  pntpbnd1  25020  pntlemc  25029  pntlemr  25036  pntlemk  25040  pntlemo  25041  abvcxp  25049  ostth2lem1  25052  padicabv  25064  ostth2lem2  25068  ostth2lem3  25069  ostth2lem4  25070  ostth2  25071  legso  25240  trgcopy  25442  nvmtri  26732  imsmetlem  26754  vacn  26762  nmcvcn  26763  smcnlem  26765  blometi  26876  ipblnfi  26929  minvecolem2  26949  hhssnv  27339  nmcoplbi  28105  nmopcoi  28172  nmopcoadji  28178  idleop  28208  cdj1i  28510  isoun  28696  xlt2addrd  28747  omndmul  28879  ogrpsub  28882  archirngz  28908  gsumle  28944  ofldchr  28979  pstmxmet  29102  nexple  29233  esumpmono  29302  esumcvg  29309  meascnbl  29443  omsmon  29521  omsmeas  29546  dstfrvinc  29699  derangenlem  30241  subfaclefac  30246  subfaclim  30258  erdszelem10  30270  sinccvglem  30654  iprodefisum  30714  unbdqndv2lem2  31505  itg2gt0cn  32459  ibladdnclem  32460  iblabsnc  32468  iblmulc2nc  32469  itgabsnc  32473  bddiblnc  32474  ftc1anclem7  32485  ftc1anclem8  32486  ftc1anc  32487  mettrifi  32547  equivbnd2  32585  heiborlem6  32609  bfplem1  32615  bfp  32617  rrnmet  32622  rrndstprj1  32623  rrndstprj2  32624  dalawlem3  34001  dalawlem4  34002  dalawlem6  34004  dalawlem9  34007  dalawlem11  34009  dalawlem12  34010  dalawlem15  34013  cdleme3c  34359  cdleme7e  34376  cdleme26e  34489  cdleme26eALTN  34491  cdleme27a  34497  cdleme32c  34573  cdleme32e  34575  cdleme32le  34577  cdlemg9b  34763  cdlemg12b  34774  cdlemg12d  34776  trlcolem  34856  trlcone  34858  cdlemk7  34978  cdlemk7u  35000  cdlemk39  35046  cdlemk11ta  35059  cdlemk11tc  35075  mapdcnvatN  35797  irrapxlem5  36232  pell1qrge1  36276  pell1qrgaplem  36279  pell14qrgapw  36282  pellqrex  36285  pellfund14  36304  expmordi  36354  jm2.17a  36369  jm2.17c  36371  acongeq  36392  jm2.19  36402  jm2.27a  36414  jm2.27c  36416  jm3.1lem2  36427  areaquad  36645  rp-isfinite6  36707  hashnzfzclim  37367  binomcxplemnotnn0  37401  ltmod  38529  dvbdfbdioolem2  38643  ioodvbdlimc1lem2  38646  ioodvbdlimc2lem  38648  stoweidlem3  38720  stoweidlem26  38743  wallispilem1  38782  wallispilem5  38786  stirlinglem1  38791  stirlinglem5  38795  stirlinglem8  38798  stirlinglem10  38800  stirlinglem12  38802  fourierdlem6  38830  fourierdlem7  38831  fourierdlem14  38838  fourierdlem19  38843  fourierdlem35  38859  fourierdlem39  38863  fourierdlem42  38866  fourierdlem50  38873  fourierdlem73  38896  fourierdlem76  38899  fourierdlem77  38900  fourierdlem81  38904  fourierdlem90  38913  fourierdlem92  38915  fourierdlem93  38916  fourierdlem111  38934  fouriersw  38948  etransclem38  38989  sge0split  39126  lighneallem4a  39888  eucrct2eupth  41435  rnghmsubcsetc  41791  rhmsubcsetc  41837  rhmsubcrngc  41843  rhmsubc  41904  rhmsubcALTV  41923  logbpw2m1  42181  dignn0flhalflem1  42229  dignn0flhalflem2  42230  amgmwlem  42340
  Copyright terms: Public domain W3C validator