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

Theorem 3brtr4d 5138
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 5119 . 2 (𝜑 → (𝐶𝑅𝐷𝐴𝑅𝐵))
51, 4mpbird 257 1 (𝜑𝐶𝑅𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542   class class class wbr 5106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107
This theorem is referenced by:  f1oiso2  7298  sucdom2OLD  9027  sucdom2  9151  ordtypelem6  9460  ttrcltr  9653  ttrclss  9657  ttrclselem2  9663  fin23lem26  10262  distrnq  10898  lediv12a  12049  recp1lt1  12054  ifle  13117  xleadd1a  13173  xlemul1a  13208  fldiv4p1lem1div2  13741  fldiv4lem1div2  13743  quoremz  13761  quoremnn0ALT  13763  intfracq  13765  modmulnn  13795  fzennn  13874  monoord2  13940  expgt1  14007  expmordi  14073  leexp2r  14080  leexp1a  14081  bernneq  14133  expmulnbnd  14139  digit1  14141  faclbnd  14191  faclbnd4lem3  14196  faclbnd4lem4  14197  faclbnd6  14200  facubnd  14201  hashdomi  14281  fzsdom2  14329  absrele  15194  absimle  15195  abstri  15216  abs2difabs  15220  limsupval2  15363  rlimrege0  15462  rlimrecl  15463  climsqz  15524  climsqz2  15525  rlimdiv  15531  rlimsqz  15535  rlimsqz2  15536  isercolllem1  15550  isercoll2  15554  fsumcvg2  15613  fsumrlim  15697  o1fsum  15699  cvgcmpce  15704  isumle  15730  climcndslem1  15735  climcndslem2  15736  harmonic  15745  expcnv  15750  explecnv  15751  geomulcvg  15762  efcllem  15961  ege2le3  15973  eflegeo  16004  rpnnen2lem4  16100  ruclem2  16115  ruclem8  16120  fsumdvds  16191  phibnd  16644  iserodd  16708  pcdvdstr  16749  pcprmpw2  16755  pockthg  16779  prmreclem4  16792  prmolefac  16919  2expltfac  16966  mod2ile  18384  odsubdvds  19354  pgpfi  19388  fislw  19408  efgredlemd  19527  efgredlem  19530  frgpcpbl  19542  abvres  20301  abvtrivd  20302  znrrg  20975  cstucnd  23639  psmetge0  23668  psmetres2  23670  xmetge0  23700  xmetres2  23717  imasf1oxmet  23731  comet  23872  stdbdxmet  23874  dscmet  23931  nrmmetd  23933  nmrtri  23983  tngngp  24021  nmolb2d  24085  nmoleub  24098  nmoco  24104  nmotri  24106  nmoid  24109  nmods  24111  cnmet  24138  xrsxmet  24175  metdstri  24217  metnrmlem3  24227  lebnumlem3  24329  ipcau2  24601  tcphcphlem1  24602  tcphcph  24604  trirn  24767  rrxmet  24775  rrxdstprj1  24776  minveclem2  24793  ovolunlem1a  24863  ovolscalem1  24880  volss  24900  voliunlem1  24917  volcn  24973  itg1climres  25082  mbfi1fseqlem5  25087  mbfi1fseqlem6  25088  itg2const2  25109  itg2seq  25110  itg2mulc  25115  itg2splitlem  25116  itg2monolem1  25118  itg2i1fseqle  25122  itg2i1fseq  25123  itg2i1fseq2  25124  itg2addlem  25126  itg2cnlem1  25129  itg2cnlem2  25130  iblss  25172  itgle  25177  ibladdlem  25187  iblabs  25196  iblabsr  25197  iblmulc2  25198  itgabs  25202  bddmulibl  25206  bddiblnc  25209  dvfsumabs  25390  dvfsumlem2  25394  dvfsum2  25401  deg1suble  25475  deg1mul3le  25484  plyeq0lem  25574  dgrcolem2  25638  geolim3  25702  aaliou3lem2  25706  aaliou3lem8  25708  ulmdvlem1  25762  radcnvlem1  25775  radcnvlem2  25776  dvradcnv  25783  pserulm  25784  pserdvlem2  25790  abelthlem2  25794  abelthlem5  25797  abelthlem7  25800  abelth2  25804  tangtx  25865  tanabsge  25866  tanord1  25896  argregt0  25968  argrege0  25969  argimgt0  25970  abslogle  25976  logcnlem4  26003  logtayllem  26017  abscxpbnd  26109  ang180lem2  26163  atanlogsublem  26268  atans2  26284  leibpi  26295  birthdaylem3  26306  cxplim  26324  cxp2limlem  26328  cxploglim2  26331  jensenlem2  26340  jensen  26341  amgmlem  26342  emcllem2  26349  emcllem4  26351  emcllem7  26354  zetacvg  26367  lgamgulmlem2  26382  lgamgulmlem5  26385  ftalem5  26429  basellem4  26436  basellem6  26438  basellem8  26440  basellem9  26441  chtwordi  26508  chpwordi  26509  ppiwordi  26514  ppiub  26555  vmalelog  26556  chtlepsi  26557  chtleppi  26561  chtublem  26562  chtub  26563  chpub  26571  logfaclbnd  26573  logfacrlim  26575  dchrptlem3  26617  bcmono  26628  bclbnd  26631  bposlem1  26635  bposlem6  26640  bposlem9  26643  lgsqrlem4  26700  2lgslem1c  26744  chebbnd1lem1  26820  chebbnd1lem3  26822  chebbnd1  26823  chtppilimlem1  26824  vmadivsum  26833  rplogsumlem2  26836  dchrisumlema  26839  dchrisumlem3  26842  dchrmusum2  26845  dchrvmasumlem3  26850  dchrvmasumiflem1  26852  dchrisum0flblem1  26859  dchrisum0re  26864  dchrisum0lem2a  26868  mulogsumlem  26882  mulog2sumlem1  26885  mulog2sumlem2  26886  2vmadivsumlem  26891  selberg2lem  26901  selberg3lem1  26908  selberg4lem1  26911  pntrlog2bndlem3  26930  pntrlog2bndlem5  26932  pntrlog2bndlem6  26934  pntpbnd1  26937  pntlemc  26946  pntlemr  26953  pntlemk  26957  pntlemo  26958  abvcxp  26966  ostth2lem1  26969  padicabv  26981  ostth2lem2  26985  ostth2lem3  26986  ostth2lem4  26987  ostth2  26988  noextendlt  27020  noextendgt  27021  nosupbnd1  27065  nosupbnd2lem1  27066  noinfbnd1  27080  noinfbnd2lem1  27081  addsproplem2  27285  addsproplem4  27287  addsproplem5  27288  addsproplem6  27289  legso  27544  trgcopy  27749  eucrct2eupth  29192  nvmtri  29616  imsmetlem  29635  vacn  29639  nmcvcn  29640  smcnlem  29642  blometi  29748  ipblnfi  29800  minvecolem2  29820  hhssnv  30209  nmcoplbi  30973  nmopcoi  31040  nmopcoadji  31046  idleop  31076  cdj1i  31378  isoun  31618  xlt2addrd  31666  mgcf1o  31866  omndmul  31925  ogrpsub  31927  gsumle  31935  cycpmconjslem2  32007  archirngz  32028  ofldchr  32112  lssdimle  32308  fedgmullem2  32328  pstmxmet  32481  nexple  32611  esumpmono  32681  esumcvg  32688  meascnbl  32821  omsmon  32901  omsmeas  32926  dstfrvinc  33079  hgt750lemd  33264  hgt750lema  33273  hgt750leme  33274  swrdwlk  33723  derangenlem  33768  subfaclefac  33773  subfaclim  33785  erdszelem10  33797  sinccvglem  34263  iprodefisum  34317  unbdqndv2lem2  34976  itg2gt0cn  36136  ibladdnclem  36137  iblabsnc  36145  iblmulc2nc  36146  itgabsnc  36150  ftc1anclem7  36160  ftc1anclem8  36161  ftc1anc  36162  mettrifi  36219  equivbnd2  36254  heiborlem6  36278  bfplem1  36284  bfp  36286  rrnmet  36291  rrndstprj1  36292  rrndstprj2  36293  dalawlem3  38339  dalawlem4  38340  dalawlem6  38342  dalawlem9  38345  dalawlem11  38347  dalawlem12  38348  dalawlem15  38351  cdleme3c  38696  cdleme7e  38713  cdleme26e  38825  cdleme26eALTN  38827  cdleme27a  38833  cdleme32c  38909  cdleme32e  38911  cdleme32le  38913  cdlemg9b  39099  cdlemg12b  39110  cdlemg12d  39112  trlcolem  39192  trlcone  39194  cdlemk7  39314  cdlemk7u  39336  cdlemk39  39382  cdlemk11ta  39395  cdlemk11tc  39411  mapdcnvatN  40132  factwoffsmonot  40618  frlmvscadiccat  40684  3cubeslem1  41010  irrapxlem5  41152  pell1qrge1  41196  pell1qrgaplem  41199  pell14qrgapw  41202  pellqrex  41205  pellfund14  41224  jm2.17a  41287  jm2.17c  41289  acongeq  41310  jm2.19  41320  jm2.27a  41332  jm2.27c  41334  jm3.1lem2  41345  areaquad  41553  rp-isfinite6  41797  hashnzfzclim  42609  binomcxplemnotnn0  42643  absimlere  43722  monoord2xrv  43726  ltmod  43886  dvbdfbdioolem2  44177  ioodvbdlimc1lem2  44180  ioodvbdlimc2lem  44182  stoweidlem3  44251  stoweidlem26  44274  wallispilem1  44313  wallispilem5  44317  stirlinglem1  44322  stirlinglem5  44326  stirlinglem8  44329  stirlinglem10  44331  stirlinglem12  44333  fourierdlem6  44361  fourierdlem7  44362  fourierdlem14  44369  fourierdlem19  44374  fourierdlem35  44390  fourierdlem39  44394  fourierdlem42  44397  fourierdlem50  44404  fourierdlem73  44427  fourierdlem76  44430  fourierdlem77  44431  fourierdlem81  44435  fourierdlem90  44444  fourierdlem92  44446  fourierdlem93  44447  fourierdlem111  44465  fouriersw  44479  etransclem38  44520  sge0split  44657  ovnsslelem  44808  lighneallem4a  45807  rnghmsubcsetc  46282  rhmsubcsetc  46328  rhmsubcrngc  46334  rhmsubc  46395  rhmsubcALTV  46413  logbpw2m1  46660  dignn0flhalflem1  46708  dignn0flhalflem2  46709  1aryenef  46738  2aryenef  46749  2itscp  46874  amgmwlem  47256
  Copyright terms: Public domain W3C validator