Theorem 3brtr4d 5143

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

Step	Hyp	Ref	Expression
1		3brtr4d.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		3brtr4d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐴)
3		3brtr4d.3	. . 3 ⊢ (𝜑 → 𝐷 = 𝐵)
4	2, 3	breq12d 5121	. 2 ⊢ (𝜑 → (𝐶𝑅𝐷 ↔ 𝐴𝑅𝐵))
5	1, 4	mpbird 260	1 ⊢ (𝜑 → 𝐶𝑅𝐷)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   class class class wbr 5108

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109

This theorem is used by:  f1oiso2  7391  sucdom2  9256  ordtypelem6  9554  ttrcltr  9754  ttrclss  9758  ttrclselem2  9764  fin23lem26  10442  distrnq  11085  lediv12a  12250  recp1lt1  12255  ifle  13367  xleadd1a  13423  xlemul1a  13458  fldiv4p1lem1div2  14015  fldiv4lem1div2  14017  quoremz  14035  quoremnn0ALT  14037  intfracq  14039  modmulnn  14069  fzennn  14151  monoord2  14216  expgt1  14283  expmordi  14350  leexp2r  14357  leexp1a  14358  bernneq  14414  expmulnbnd  14420  digit1  14422  faclbnd  14475  faclbnd4lem3  14480  faclbnd4lem4  14481  faclbnd6  14484  facubnd  14485  hashdomi  14565  fzsdom2  14614  absrele  15518  absimle  15519  abstri  15541  abs2difabs  15545  limsupval2  15691  rlimrege0  15790  rlimrecl  15791  climsqz  15852  climsqz2  15853  rlimdiv  15857  rlimsqz  15861  rlimsqz2  15862  isercolllem1  15876  isercoll2  15880  fsumcvg2  15937  fsumrlim  16022  o1fsum  16024  cvgcmpce  16029  isumle  16057  climcndslem1  16062  climcndslem2  16063  harmonic  16072  expcnv  16077  explecnv  16078  geomulcvg  16089  efcllem  16287  ege2le3  16300  eflegeo  16333  rpnnen2lem4  16429  ruclem2  16444  ruclem8  16449  fsumdvds  16522  phibnd  16992  iserodd  17057  pcdvdstr  17098  pcprmpw2  17104  pockthg  17128  prmreclem4  17141  prmolefac  17268  2expltfac  17314  mod2ile  18718  pfxchn  18834  chnub  18846  chnccats1  18849  chnccat  18850  chnrev  18851  ex-chn2  18862  odsubdvds  19836  pgpfi  19870  fislw  19890  efgredlemd  20009  efgredlem  20012  frgpcpbl  20024  omndmul  20400  ogrpsub  20402  gsumle  20410  rnghmsubcsetc  20936  rhmsubcsetc  20965  rhmsubcrngc  20971  rhmsubc  20992  abvres  21139  abvtrivd  21140  znrrg  21926  ofldchr  21937  cstucnd  24657  psmetge0  24686  psmetres2  24688  xmetge0  24718  xmetres2  24735  imasf1oxmet  24749  comet  24887  stdbdxmet  24889  dscmet  24946  nrmmetd  24948  nmrtri  24998  tngngp  25028  nmolb2d  25092  nmoleub  25105  nmoco  25111  nmotri  25113  nmoid  25116  nmods  25118  cnmet  25145  xrsxmet  25184  metdstri  25226  metnrmlem3  25236  lebnumlem3  25339  ipcau2  25610  tcphcphlem1  25611  tcphcph  25613  trirn  25776  rrxmet  25784  rrxdstprj1  25785  minveclem2  25802  ovolunlem1a  25872  ovolscalem1  25889  volss  25909  voliunlem1  25926  volcn  25982  itg1climres  26090  mbfi1fseqlem5  26095  mbfi1fseqlem6  26096  itg2const2  26117  itg2seq  26118  itg2mulc  26123  itg2splitlem  26124  itg2monolem1  26126  itg2i1fseqle  26130  itg2i1fseq  26131  itg2i1fseq2  26132  itg2addlem  26134  itg2cnlem1  26137  itg2cnlem2  26138  iblss  26180  itgle  26185  ibladdlem  26195  iblabs  26204  iblabsr  26205  iblmulc2  26206  itgabs  26210  bddmulibl  26214  bddiblnc  26217  dvfsumabs  26398  dvfsumlem2  26402  dvfsum2  26409  deg1suble  26480  deg1mul3le  26490  plyeq0lem  26584  dgrcolem2  26648  geolim3  26723  aaliou3lem2  26727  aaliou3lem8  26729  ulmdvlem1  26784  radcnvlem1  26797  radcnvlem2  26798  dvradcnv  26805  pserulm  26806  pserdvlem2  26812  abelthlem2  26816  abelthlem5  26819  abelthlem7  26822  abelth2  26826  tangtx  26891  tanabsge  26892  tanord1  26922  argregt0  26995  argrege0  26996  argimgt0  26997  abslogle  27003  logcnlem4  27030  logtayllem  27044  abscxpbnd  27138  ang180lem2  27195  atanlogsublem  27300  atans2  27316  leibpi  27327  birthdaylem3  27338  cxplim  27356  cxp2limlem  27360  cxploglim2  27363  jensenlem2  27372  jensen  27373  amgmlem  27374  emcllem2  27381  emcllem4  27383  emcllem7  27386  zetacvg  27399  lgamgulmlem2  27414  lgamgulmlem5  27417  ftalem5  27461  basellem4  27468  basellem6  27470  basellem8  27472  basellem9  27473  chtwordi  27540  chpwordi  27541  ppiwordi  27546  ppiub  27588  vmalelog  27589  chtlepsi  27590  chtleppi  27594  chtublem  27595  chtub  27596  chpub  27604  logfaclbnd  27606  logfacrlim  27608  dchrptlem3  27650  bcmono  27661  bclbnd  27664  bposlem1  27668  bposlem6  27673  bposlem9  27676  lgsqrlem4  27733  2lgslem1c  27777  chebbnd1lem1  27853  chebbnd1lem3  27855  chebbnd1  27856  chtppilimlem1  27857  vmadivsum  27866  rplogsumlem2  27869  dchrisumlema  27872  dchrisumlem3  27875  dchrmusum2  27878  dchrvmasumlem3  27883  dchrvmasumiflem1  27885  dchrisum0flblem1  27892  dchrisum0re  27897  dchrisum0lem2a  27901  mulogsumlem  27915  mulog2sumlem1  27918  mulog2sumlem2  27919  2vmadivsumlem  27924  selberg2lem  27934  selberg3lem1  27941  selberg4lem1  27944  pntrlog2bndlem3  27963  pntrlog2bndlem5  27965  pntrlog2bndlem6  27967  pntpbnd1  27970  pntlemc  27979  pntlemr  27986  pntlemk  27990  pntlemo  27991  abvcxp  27999  ostth2lem1  28002  padicabv  28014  ostth2lem2  28018  ostth2lem3  28019  ostth2lem4  28020  ostth2  28021  noextendlt  28083  noextendgt  28084  nosupbnd1  28128  nosupbnd2lem1  28129  noinfbnd1  28143  noinfbnd2lem1  28144  lltr  28305  addsproplem2  28413  addsproplem4  28415  addsproplem5  28416  addsproplem6  28417  mulsproplem5  28563  mulsproplem6  28564  mulsproplem7  28565  mulsproplem8  28566  lemulsd  28581  mulsuniflem  28592  lemuls1ad  28625  precsexlem9  28658  bdaypw2n0bndlem  28906  legso  29119  trgcopy  29368  cgraer  29434  angmgmaddov1  29445  angmgmaddov2  29446  swrdwlk  30325  eucrct2eupth  30903  nvmtri  31330  imsmetlem  31349  vacn  31353  nmcvcn  31354  smcnlem  31356  blometi  31462  ipblnfi  31514  minvecolem2  31534  hhssnv  31923  nmcoplbi  32687  nmopcoi  32754  nmopcoadji  32760  idleop  32790  cdj1i  33092  isoun  33392  xlt2addrd  33447  nexple  33520  mgcf1o  33663  cycpmconjslem2  33815  archirngz  33849  elrgspnlem1  33902  zzedom  33958  ply1edom  33959  q1pvsca  34241  lssdimle  34351  fedgmullem2  34373  fldextrspundglemul  34422  extdgfialglem1  34435  fldext2chn  34471  2sqr3minply  34523  cos9thpiminply  34531  pstmxmet  34640  esumpmono  34822  esumcvg  34829  meascnbl  34963  omsmon  35041  omsmeas  35066  dstfrvinc  35220  hgt750lemd  35388  hgt750lema  35397  hgt750leme  35398  derangenlem  36144  subfaclefac  36149  subfaclim  36161  erdszelem10  36173  sinccvglem  36645  iprodefisum  36721  unbdqndv2lem2  37591  itg2gt0cn  38861  ibladdnclem  38862  iblabsnc  38870  iblmulc2nc  38871  itgabsnc  38875  ftc1anclem7  38885  ftc1anclem8  38886  ftc1anc  38887  mettrifi  38957  equivbnd2  38992  heiborlem6  39016  bfplem1  39022  bfp  39024  rrnmet  39029  rrndstprj1  39030  rrndstprj2  39031  dalawlem3  41196  dalawlem4  41197  dalawlem6  41199  dalawlem9  41202  dalawlem11  41204  dalawlem12  41205  dalawlem15  41208  cdleme3c  41553  cdleme7e  41570  cdleme26e  41682  cdleme26eALTN  41684  cdleme27a  41690  cdleme32c  41766  cdleme32e  41768  cdleme32le  41770  cdlemg9b  41956  cdlemg12b  41967  cdlemg12d  41969  trlcolem  42049  trlcone  42051  cdlemk7  42171  cdlemk7u  42193  cdlemk39  42239  cdlemk11ta  42252  cdlemk11tc  42268  mapdcnvatN  42989  explt1d  43646  frlmvscadiccat  43839  3cubeslem1  43960  irrapxlem5  44099  pell1qrge1  44143  pell1qrgaplem  44146  pell14qrgapw  44149  pellqrex  44152  pellfund14  44171  jm2.17a  44233  jm2.17c  44235  acongeq  44256  jm2.19  44266  jm2.27a  44278  jm2.27c  44280  jm3.1lem2  44291  areaquad  44479  rp-isfinite6  44780  hashnzfzclim  45567  binomcxplemnotnn0  45601  absimlere  46762  monoord2xrv  46766  ltmod  46921  liminflelimsuplem  47058  dvbdfbdioolem2  47212  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  stoweidlem3  47286  stoweidlem26  47309  wallispilem1  47348  wallispilem5  47352  stirlinglem1  47357  stirlinglem5  47361  stirlinglem8  47364  stirlinglem10  47366  stirlinglem12  47368  fourierdlem6  47396  fourierdlem7  47397  fourierdlem14  47404  fourierdlem19  47409  fourierdlem35  47425  fourierdlem39  47429  fourierdlem42  47432  fourierdlem50  47439  fourierdlem73  47462  fourierdlem76  47465  fourierdlem77  47466  fourierdlem81  47470  fourierdlem90  47479  fourierdlem92  47481  fourierdlem93  47482  fourierdlem111  47500  fouriersw  47514  etransclem38  47555  sge0split  47692  ovnsslelem  47843  chnsubseq  48163  chnsuslle  48164  chnerlem1  48165  lighneallem4a  48966  rhmsubcALTV  49655  logbpw2m1  50010  dignn0flhalflem1  50058  dignn0flhalflem2  50059  1aryenef  50088  2aryenef  50099  2itscp  50224  amgmwlem  51415