Theorem 3brtr4d 5098

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

Syntax hints:   → wi 4   = wceq 1537   class class class wbr 5066

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 2793

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 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067

This theorem is referenced by:  f1oiso2  7105  sucdom2  8714  ordtypelem6  8987  fin23lem26  9747  distrnq  10383  lediv12a  11533  recp1lt1  11538  ifle  12591  xleadd1a  12647  xlemul1a  12682  fldiv4p1lem1div2  13206  fldiv4lem1div2  13208  quoremz  13224  quoremnn0ALT  13226  intfracq  13228  modmulnn  13258  fzennn  13337  monoord2  13402  expgt1  13468  expmordi  13532  leexp2r  13539  leexp1a  13540  bernneq  13591  expmulnbnd  13597  digit1  13599  faclbnd  13651  faclbnd4lem3  13656  faclbnd4lem4  13657  faclbnd6  13660  facubnd  13661  hashdomi  13742  fzsdom2  13790  absrele  14668  absimle  14669  abstri  14690  abs2difabs  14694  limsupval2  14837  rlimrege0  14936  rlimrecl  14937  climsqz  14997  climsqz2  14998  rlimdiv  15002  rlimsqz  15006  rlimsqz2  15007  isercolllem1  15021  isercoll2  15025  fsumcvg2  15084  fsumrlim  15166  o1fsum  15168  cvgcmpce  15173  isumle  15199  climcndslem1  15204  climcndslem2  15205  harmonic  15214  expcnv  15219  explecnv  15220  geomulcvg  15232  efcllem  15431  ege2le3  15443  eflegeo  15474  rpnnen2lem4  15570  ruclem2  15585  ruclem8  15590  fsumdvds  15658  phibnd  16108  iserodd  16172  pcdvdstr  16212  pcprmpw2  16218  pockthg  16242  prmreclem4  16255  prmolefac  16382  2expltfac  16426  mod2ile  17716  odsubdvds  18696  pgpfi  18730  fislw  18750  efgredlemd  18870  efgredlem  18873  frgpcpbl  18885  abvres  19610  abvtrivd  19611  znrrg  20712  cstucnd  22893  psmetge0  22922  psmetres2  22924  xmetge0  22954  xmetres2  22971  imasf1oxmet  22985  comet  23123  stdbdxmet  23125  dscmet  23182  nrmmetd  23184  nmrtri  23233  tngngp  23263  nmolb2d  23327  nmoleub  23340  nmoco  23346  nmotri  23348  nmoid  23351  nmods  23353  cnmet  23380  xrsxmet  23417  metdstri  23459  metnrmlem3  23469  lebnumlem3  23567  ipcau2  23837  tcphcphlem1  23838  tcphcph  23840  trirn  24003  rrxmet  24011  rrxdstprj1  24012  minveclem2  24029  ovolunlem1a  24097  ovolscalem1  24114  volss  24134  voliunlem1  24151  volcn  24207  itg1climres  24315  mbfi1fseqlem5  24320  mbfi1fseqlem6  24321  itg2const2  24342  itg2seq  24343  itg2mulc  24348  itg2splitlem  24349  itg2monolem1  24351  itg2i1fseqle  24355  itg2i1fseq  24356  itg2i1fseq2  24357  itg2addlem  24359  itg2cnlem1  24362  itg2cnlem2  24363  iblss  24405  itgle  24410  ibladdlem  24420  iblabs  24429  iblabsr  24430  iblmulc2  24431  itgabs  24435  bddmulibl  24439  dvfsumabs  24620  dvfsumlem2  24624  dvfsum2  24631  deg1suble  24701  deg1mul3le  24710  plyeq0lem  24800  dgrcolem2  24864  geolim3  24928  aaliou3lem2  24932  aaliou3lem8  24934  ulmdvlem1  24988  radcnvlem1  25001  radcnvlem2  25002  dvradcnv  25009  pserulm  25010  pserdvlem2  25016  abelthlem2  25020  abelthlem5  25023  abelthlem7  25026  abelth2  25030  tangtx  25091  tanabsge  25092  tanord1  25121  argregt0  25193  argrege0  25194  argimgt0  25195  abslogle  25201  logcnlem4  25228  logtayllem  25242  abscxpbnd  25334  ang180lem2  25388  atanlogsublem  25493  atans2  25509  leibpi  25520  birthdaylem3  25531  cxplim  25549  cxp2limlem  25553  cxploglim2  25556  jensenlem2  25565  jensen  25566  amgmlem  25567  emcllem2  25574  emcllem4  25576  emcllem7  25579  zetacvg  25592  lgamgulmlem2  25607  lgamgulmlem5  25610  ftalem5  25654  basellem4  25661  basellem6  25663  basellem8  25665  basellem9  25666  chtwordi  25733  chpwordi  25734  ppiwordi  25739  ppiub  25780  vmalelog  25781  chtlepsi  25782  chtleppi  25786  chtublem  25787  chtub  25788  chpub  25796  logfaclbnd  25798  logfacrlim  25800  dchrptlem3  25842  bcmono  25853  bclbnd  25856  bposlem1  25860  bposlem6  25865  bposlem9  25868  lgsqrlem4  25925  2lgslem1c  25969  chebbnd1lem1  26045  chebbnd1lem3  26047  chebbnd1  26048  chtppilimlem1  26049  vmadivsum  26058  rplogsumlem2  26061  dchrisumlema  26064  dchrisumlem3  26067  dchrmusum2  26070  dchrvmasumlem3  26075  dchrvmasumiflem1  26077  dchrisum0flblem1  26084  dchrisum0re  26089  dchrisum0lem2a  26093  mulogsumlem  26107  mulog2sumlem1  26110  mulog2sumlem2  26111  2vmadivsumlem  26116  selberg2lem  26126  selberg3lem1  26133  selberg4lem1  26136  pntrlog2bndlem3  26155  pntrlog2bndlem5  26157  pntrlog2bndlem6  26159  pntpbnd1  26162  pntlemc  26171  pntlemr  26178  pntlemk  26182  pntlemo  26183  abvcxp  26191  ostth2lem1  26194  padicabv  26206  ostth2lem2  26210  ostth2lem3  26211  ostth2lem4  26212  ostth2  26213  legso  26385  trgcopy  26590  eucrct2eupth  28024  nvmtri  28448  imsmetlem  28467  vacn  28471  nmcvcn  28472  smcnlem  28474  blometi  28580  ipblnfi  28632  minvecolem2  28652  hhssnv  29041  nmcoplbi  29805  nmopcoi  29872  nmopcoadji  29878  idleop  29908  cdj1i  30210  isoun  30437  xlt2addrd  30482  omndmul  30715  ogrpsub  30717  gsumle  30725  cycpmconjslem2  30797  archirngz  30818  ofldchr  30887  lssdimle  31006  fedgmullem2  31026  pstmxmet  31137  nexple  31268  esumpmono  31338  esumcvg  31345  meascnbl  31478  omsmon  31556  omsmeas  31581  dstfrvinc  31734  hgt750lemd  31919  hgt750lema  31928  hgt750leme  31929  swrdwlk  32373  derangenlem  32418  subfaclefac  32423  subfaclim  32435  erdszelem10  32447  sinccvglem  32915  iprodefisum  32973  noextendlt  33176  noextendgt  33177  nosupbnd1  33214  nosupbnd2lem1  33215  unbdqndv2lem2  33849  itg2gt0cn  34962  ibladdnclem  34963  iblabsnc  34971  iblmulc2nc  34972  itgabsnc  34976  bddiblnc  34977  ftc1anclem7  34988  ftc1anclem8  34989  ftc1anc  34990  mettrifi  35047  equivbnd2  35085  heiborlem6  35109  bfplem1  35115  bfp  35117  rrnmet  35122  rrndstprj1  35123  rrndstprj2  35124  dalawlem3  37024  dalawlem4  37025  dalawlem6  37027  dalawlem9  37030  dalawlem11  37032  dalawlem12  37033  dalawlem15  37036  cdleme3c  37381  cdleme7e  37398  cdleme26e  37510  cdleme26eALTN  37512  cdleme27a  37518  cdleme32c  37594  cdleme32e  37596  cdleme32le  37598  cdlemg9b  37784  cdlemg12b  37795  cdlemg12d  37797  trlcolem  37877  trlcone  37879  cdlemk7  37999  cdlemk7u  38021  cdlemk39  38067  cdlemk11ta  38080  cdlemk11tc  38096  mapdcnvatN  38817  factwoffsmonot  39147  frlmvscadiccat  39194  3cubeslem1  39330  irrapxlem5  39472  pell1qrge1  39516  pell1qrgaplem  39519  pell14qrgapw  39522  pellqrex  39525  pellfund14  39544  jm2.17a  39606  jm2.17c  39608  acongeq  39629  jm2.19  39639  jm2.27a  39651  jm2.27c  39653  jm3.1lem2  39664  areaquad  39872  rp-isfinite6  39933  hashnzfzclim  40703  binomcxplemnotnn0  40737  absimlere  41805  monoord2xrv  41809  ltmod  41968  dvbdfbdioolem2  42263  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  stoweidlem3  42337  stoweidlem26  42360  wallispilem1  42399  wallispilem5  42403  stirlinglem1  42408  stirlinglem5  42412  stirlinglem8  42415  stirlinglem10  42417  stirlinglem12  42419  fourierdlem6  42447  fourierdlem7  42448  fourierdlem14  42455  fourierdlem19  42460  fourierdlem35  42476  fourierdlem39  42480  fourierdlem42  42483  fourierdlem50  42490  fourierdlem73  42513  fourierdlem76  42516  fourierdlem77  42517  fourierdlem81  42521  fourierdlem90  42530  fourierdlem92  42532  fourierdlem93  42533  fourierdlem111  42551  fouriersw  42565  etransclem38  42606  sge0split  42740  lighneallem4a  43822  rnghmsubcsetc  44297  rhmsubcsetc  44343  rhmsubcrngc  44349  rhmsubc  44410  rhmsubcALTV  44428  logbpw2m1  44676  dignn0flhalflem1  44724  dignn0flhalflem2  44725  2itscp  44817  amgmwlem  44952