Theorem 3brtr4d 5137

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 5116	. 2 ⊢ (𝜑 → (𝐶𝑅𝐷 ↔ 𝐴𝑅𝐵))
5	1, 4	mpbird 260	1 ⊢ (𝜑 → 𝐶𝑅𝐷)

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

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 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104

This theorem is used by:  f1oiso2  7358  sucdom2  9211  ordtypelem6  9510  ttrcltr  9710  ttrclss  9714  ttrclselem2  9720  fin23lem26  10396  distrnq  11039  lediv12a  12203  recp1lt1  12208  ifle  13320  xleadd1a  13376  xlemul1a  13411  fldiv4p1lem1div2  13968  fldiv4lem1div2  13970  quoremz  13988  quoremnn0ALT  13990  intfracq  13992  modmulnn  14022  fzennn  14104  monoord2  14169  expgt1  14236  expmordi  14303  leexp2r  14310  leexp1a  14311  bernneq  14366  expmulnbnd  14372  digit1  14374  faclbnd  14427  faclbnd4lem3  14432  faclbnd4lem4  14433  faclbnd6  14436  facubnd  14437  hashdomi  14517  fzsdom2  14566  absrele  15468  absimle  15469  abstri  15491  abs2difabs  15495  limsupval2  15640  rlimrege0  15739  rlimrecl  15740  climsqz  15801  climsqz2  15802  rlimdiv  15806  rlimsqz  15810  rlimsqz2  15811  isercolllem1  15825  isercoll2  15829  fsumcvg2  15886  fsumrlim  15971  o1fsum  15973  cvgcmpce  15978  isumle  16006  climcndslem1  16011  climcndslem2  16012  harmonic  16021  expcnv  16026  explecnv  16027  geomulcvg  16038  efcllem  16236  ege2le3  16249  eflegeo  16282  rpnnen2lem4  16378  ruclem2  16393  ruclem8  16398  fsumdvds  16471  phibnd  16941  iserodd  17006  pcdvdstr  17047  pcprmpw2  17053  pockthg  17077  prmreclem4  17090  prmolefac  17217  2expltfac  17263  mod2ile  18661  pfxchn  18777  chnub  18789  chnccats1  18792  chnccat  18793  chnrev  18794  ex-chn2  18805  odsubdvds  19778  pgpfi  19812  fislw  19832  efgredlemd  19951  efgredlem  19954  frgpcpbl  19966  omndmul  20342  ogrpsub  20344  gsumle  20352  rnghmsubcsetc  20878  rhmsubcsetc  20907  rhmsubcrngc  20913  rhmsubc  20934  abvres  21081  abvtrivd  21082  znrrg  21864  ofldchr  21875  cstucnd  24595  psmetge0  24624  psmetres2  24626  xmetge0  24656  xmetres2  24673  imasf1oxmet  24687  comet  24825  stdbdxmet  24827  dscmet  24884  nrmmetd  24886  nmrtri  24936  tngngp  24966  nmolb2d  25030  nmoleub  25043  nmoco  25049  nmotri  25051  nmoid  25054  nmods  25056  cnmet  25083  xrsxmet  25122  metdstri  25164  metnrmlem3  25174  lebnumlem3  25277  ipcau2  25548  tcphcphlem1  25549  tcphcph  25551  trirn  25714  rrxmet  25722  rrxdstprj1  25723  minveclem2  25740  ovolunlem1a  25810  ovolscalem1  25827  volss  25847  voliunlem1  25864  volcn  25920  itg1climres  26028  mbfi1fseqlem5  26033  mbfi1fseqlem6  26034  itg2const2  26055  itg2seq  26056  itg2mulc  26061  itg2splitlem  26062  itg2monolem1  26064  itg2i1fseqle  26068  itg2i1fseq  26069  itg2i1fseq2  26070  itg2addlem  26072  itg2cnlem1  26075  itg2cnlem2  26076  iblss  26118  itgle  26123  ibladdlem  26133  iblabs  26142  iblabsr  26143  iblmulc2  26144  itgabs  26148  bddmulibl  26152  bddiblnc  26155  dvfsumabs  26336  dvfsumlem2  26340  dvfsum2  26347  deg1suble  26418  deg1mul3le  26428  plyeq0lem  26522  dgrcolem2  26586  geolim3  26659  aaliou3lem2  26663  aaliou3lem8  26665  ulmdvlem1  26720  radcnvlem1  26733  radcnvlem2  26734  dvradcnv  26741  pserulm  26742  pserdvlem2  26748  abelthlem2  26752  abelthlem5  26755  abelthlem7  26758  abelth2  26762  tangtx  26827  tanabsge  26828  tanord1  26858  argregt0  26931  argrege0  26932  argimgt0  26933  abslogle  26939  logcnlem4  26966  logtayllem  26980  abscxpbnd  27074  ang180lem2  27131  atanlogsublem  27236  atans2  27252  leibpi  27263  birthdaylem3  27274  cxplim  27292  cxp2limlem  27296  cxploglim2  27299  jensenlem2  27308  jensen  27309  amgmlem  27310  emcllem2  27317  emcllem4  27319  emcllem7  27322  zetacvg  27335  lgamgulmlem2  27350  lgamgulmlem5  27353  ftalem5  27397  basellem4  27404  basellem6  27406  basellem8  27408  basellem9  27409  chtwordi  27476  chpwordi  27477  ppiwordi  27482  ppiub  27524  vmalelog  27525  chtlepsi  27526  chtleppi  27530  chtublem  27531  chtub  27532  chpub  27540  logfaclbnd  27542  logfacrlim  27544  dchrptlem3  27586  bcmono  27597  bclbnd  27600  bposlem1  27604  bposlem6  27609  bposlem9  27612  lgsqrlem4  27669  2lgslem1c  27713  chebbnd1lem1  27789  chebbnd1lem3  27791  chebbnd1  27792  chtppilimlem1  27793  vmadivsum  27802  rplogsumlem2  27805  dchrisumlema  27808  dchrisumlem3  27811  dchrmusum2  27814  dchrvmasumlem3  27819  dchrvmasumiflem1  27821  dchrisum0flblem1  27828  dchrisum0re  27833  dchrisum0lem2a  27837  mulogsumlem  27851  mulog2sumlem1  27854  mulog2sumlem2  27855  2vmadivsumlem  27860  selberg2lem  27870  selberg3lem1  27877  selberg4lem1  27880  pntrlog2bndlem3  27899  pntrlog2bndlem5  27901  pntrlog2bndlem6  27903  pntpbnd1  27906  pntlemc  27915  pntlemr  27922  pntlemk  27926  pntlemo  27927  abvcxp  27935  ostth2lem1  27938  padicabv  27950  ostth2lem2  27954  ostth2lem3  27955  ostth2lem4  27956  ostth2  27957  noextendlt  28019  noextendgt  28020  nosupbnd1  28064  nosupbnd2lem1  28065  noinfbnd1  28079  noinfbnd2lem1  28080  lltr  28241  addsproplem2  28349  addsproplem4  28351  addsproplem5  28352  addsproplem6  28353  mulsproplem5  28499  mulsproplem6  28500  mulsproplem7  28501  mulsproplem8  28502  lemulsd  28517  mulsuniflem  28528  lemuls1ad  28561  precsexlem9  28594  bdaypw2n0bndlem  28842  legso  29055  trgcopy  29304  cgraer  29370  angmgmaddov1  29381  angmgmaddov2  29382  swrdwlk  30261  eucrct2eupth  30839  nvmtri  31266  imsmetlem  31285  vacn  31289  nmcvcn  31290  smcnlem  31292  blometi  31398  ipblnfi  31450  minvecolem2  31470  hhssnv  31859  nmcoplbi  32623  nmopcoi  32690  nmopcoadji  32696  idleop  32726  cdj1i  33028  isoun  33288  xlt2addrd  33344  nexple  33417  mgcf1o  33557  cycpmconjslem2  33709  archirngz  33743  elrgspnlem1  33796  q1pvsca  34129  lssdimle  34233  fedgmullem2  34255  fldextrspundglemul  34304  extdgfialglem1  34317  fldext2chn  34353  2sqr3minply  34405  cos9thpiminply  34413  pstmxmet  34522  esumpmono  34704  esumcvg  34711  meascnbl  34845  omsmon  34923  omsmeas  34948  dstfrvinc  35102  hgt750lemd  35270  hgt750lema  35279  hgt750leme  35280  derangenlem  35915  subfaclefac  35920  subfaclim  35932  erdszelem10  35944  sinccvglem  36416  iprodefisum  36485  unbdqndv2lem2  37356  itg2gt0cn  38573  ibladdnclem  38574  iblabsnc  38582  iblmulc2nc  38583  itgabsnc  38587  ftc1anclem7  38597  ftc1anclem8  38598  ftc1anc  38599  mettrifi  38671  equivbnd2  38706  heiborlem6  38730  bfplem1  38736  bfp  38738  rrnmet  38743  rrndstprj1  38744  rrndstprj2  38745  dalawlem3  40910  dalawlem4  40911  dalawlem6  40913  dalawlem9  40916  dalawlem11  40918  dalawlem12  40919  dalawlem15  40922  cdleme3c  41267  cdleme7e  41284  cdleme26e  41396  cdleme26eALTN  41398  cdleme27a  41404  cdleme32c  41480  cdleme32e  41482  cdleme32le  41484  cdlemg9b  41670  cdlemg12b  41681  cdlemg12d  41683  trlcolem  41763  trlcone  41765  cdlemk7  41885  cdlemk7u  41907  cdlemk39  41953  cdlemk11ta  41966  cdlemk11tc  41982  mapdcnvatN  42703  explt1d  43360  frlmvscadiccat  43553  3cubeslem1  43674  irrapxlem5  43812  pell1qrge1  43856  pell1qrgaplem  43859  pell14qrgapw  43862  pellqrex  43865  pellfund14  43884  jm2.17a  43946  jm2.17c  43948  acongeq  43969  jm2.19  43979  jm2.27a  43991  jm2.27c  43993  jm3.1lem2  44004  areaquad  44202  rp-isfinite6  44503  hashnzfzclim  45291  binomcxplemnotnn0  45325  absimlere  46458  monoord2xrv  46462  ltmod  46617  liminflelimsuplem  46754  dvbdfbdioolem2  46908  ioodvbdlimc1lem2  46911  ioodvbdlimc2lem  46913  stoweidlem3  46982  stoweidlem26  47005  wallispilem1  47044  wallispilem5  47048  stirlinglem1  47053  stirlinglem5  47057  stirlinglem8  47060  stirlinglem10  47062  stirlinglem12  47064  fourierdlem6  47092  fourierdlem7  47093  fourierdlem14  47100  fourierdlem19  47105  fourierdlem35  47121  fourierdlem39  47125  fourierdlem42  47128  fourierdlem50  47135  fourierdlem73  47158  fourierdlem76  47161  fourierdlem77  47162  fourierdlem81  47166  fourierdlem90  47175  fourierdlem92  47177  fourierdlem93  47178  fourierdlem111  47196  fouriersw  47210  etransclem38  47251  sge0split  47388  ovnsslelem  47539  chnsubseq  47859  chnsuslle  47860  chnerlem1  47861  lighneallem4a  48662  rhmsubcALTV  49351  logbpw2m1  49648  dignn0flhalflem1  49696  dignn0flhalflem2  49697  1aryenef  49726  2aryenef  49737  2itscp  49862  amgmwlem  50956