Theorem 3brtr4d 4918

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

Syntax hints:   → wi 4   = wceq 1601   class class class wbr 4886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-rab 3098  df-v 3399  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-nul 4141  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-br 4887

This theorem is referenced by:  f1oiso2  6874  sucdom2  8444  ordtypelem6  8717  cdaen  9330  cdacomen  9338  cdadom1  9343  fin23lem26  9482  distrnq  10118  lediv12a  11270  recp1lt1  11275  ifle  12340  xleadd1a  12395  xlemul1a  12430  fldiv4p1lem1div2  12955  fldiv4lem1div2  12957  quoremz  12973  quoremnn0ALT  12975  intfracq  12977  modmulnn  13007  fzennn  13086  monoord2  13150  expgt1  13216  leexp2r  13236  leexp1a  13237  bernneq  13309  expmulnbnd  13315  digit1  13317  faclbnd  13395  faclbnd4lem3  13400  faclbnd4lem4  13401  faclbnd6  13404  facubnd  13405  hashdomi  13484  fzsdom2  13529  absrele  14455  absimle  14456  abstri  14477  abs2difabs  14481  limsupval2  14619  rlimrege0  14718  rlimrecl  14719  climsqz  14779  climsqz2  14780  rlimdiv  14784  rlimsqz  14788  rlimsqz2  14789  isercolllem1  14803  isercoll2  14807  fsumcvg2  14865  fsumrlim  14947  o1fsum  14949  cvgcmpce  14954  isumle  14980  climcndslem1  14985  climcndslem2  14986  harmonic  14995  expcnv  15000  explecnv  15001  geomulcvg  15011  efcllem  15210  ege2le3  15222  eflegeo  15253  rpnnen2lem4  15350  ruclem2  15365  ruclem8  15370  fsumdvds  15437  phibnd  15880  iserodd  15944  pcdvdstr  15984  pcprmpw2  15990  pockthg  16014  prmreclem4  16027  prmolefac  16154  2expltfac  16198  mod2ile  17492  odsubdvds  18370  pgpfi  18404  fislw  18424  efgredlemd  18542  efgredlem  18545  efgredlemOLD  18546  frgpcpbl  18558  abvres  19231  abvtrivd  19232  znrrg  20309  cstucnd  22496  psmetge0  22525  psmetres2  22527  xmetge0  22557  xmetres2  22574  imasf1oxmet  22588  comet  22726  stdbdxmet  22728  dscmet  22785  nrmmetd  22787  nmrtri  22836  tngngp  22866  nmolb2d  22930  nmoleub  22943  nmoco  22949  nmotri  22951  nmoid  22954  nmods  22956  cnmet  22983  xrsxmet  23020  metdstri  23062  metnrmlem3  23072  lebnumlem3  23170  ipcau2  23440  tcphcphlem1  23441  tcphcph  23443  trirn  23606  rrxmet  23614  rrxdstprj1  23615  minveclem2  23632  ovolunlem1a  23700  ovolscalem1  23717  volss  23737  voliunlem1  23754  volcn  23810  itg1climres  23918  mbfi1fseqlem5  23923  mbfi1fseqlem6  23924  itg2const2  23945  itg2seq  23946  itg2mulc  23951  itg2splitlem  23952  itg2monolem1  23954  itg2i1fseqle  23958  itg2i1fseq  23959  itg2i1fseq2  23960  itg2addlem  23962  itg2cnlem1  23965  itg2cnlem2  23966  iblss  24008  itgle  24013  ibladdlem  24023  iblabs  24032  iblabsr  24033  iblmulc2  24034  itgabs  24038  bddmulibl  24042  dvfsumabs  24223  dvfsumlem2  24227  dvfsum2  24234  deg1suble  24304  deg1mul3le  24313  plyeq0lem  24403  dgrcolem2  24467  geolim3  24531  aaliou3lem2  24535  aaliou3lem8  24537  ulmdvlem1  24591  radcnvlem1  24604  radcnvlem2  24605  dvradcnv  24612  pserulm  24613  pserdvlem2  24619  abelthlem2  24623  abelthlem5  24626  abelthlem7  24629  abelth2  24633  tangtx  24695  tanabsge  24696  tanord1  24721  argregt0  24793  argrege0  24794  argimgt0  24795  abslogle  24801  logcnlem4  24828  logtayllem  24842  abscxpbnd  24934  ang180lem2  24988  atanlogsublem  25093  atans2  25109  leibpi  25121  birthdaylem3  25132  cxplim  25150  cxp2limlem  25154  cxploglim2  25157  jensenlem2  25166  jensen  25167  amgmlem  25168  emcllem2  25175  emcllem4  25177  emcllem7  25180  zetacvg  25193  lgamgulmlem2  25208  lgamgulmlem5  25211  lgamcvg2  25233  ftalem5  25255  basellem4  25262  basellem6  25264  basellem8  25266  basellem9  25267  chtwordi  25334  chpwordi  25335  ppiwordi  25340  ppiub  25381  vmalelog  25382  chtlepsi  25383  chtleppi  25387  chtublem  25388  chtub  25389  chpub  25397  logfaclbnd  25399  logfacrlim  25401  dchrptlem3  25443  bcmono  25454  bclbnd  25457  bposlem1  25461  bposlem6  25466  bposlem9  25469  lgsqrlem4  25526  2lgslem1c  25570  chebbnd1lem1  25610  chebbnd1lem3  25612  chebbnd1  25613  chtppilimlem1  25614  vmadivsum  25623  rplogsumlem2  25626  dchrisumlema  25629  dchrisumlem3  25632  dchrmusum2  25635  dchrvmasumlem3  25640  dchrvmasumiflem1  25642  dchrisum0flblem1  25649  dchrisum0re  25654  dchrisum0lem2a  25658  mulogsumlem  25672  mulog2sumlem1  25675  mulog2sumlem2  25676  2vmadivsumlem  25681  selberg2lem  25691  selberg3lem1  25698  selberg4lem1  25701  pntrlog2bndlem3  25720  pntrlog2bndlem5  25722  pntrlog2bndlem6  25724  pntpbnd1  25727  pntlemc  25736  pntlemr  25743  pntlemk  25747  pntlemo  25748  abvcxp  25756  ostth2lem1  25759  padicabv  25771  ostth2lem2  25775  ostth2lem3  25776  ostth2lem4  25777  ostth2  25778  legso  25950  trgcopy  26152  eucrct2eupthOLD  27664  eucrct2eupth  27665  nvmtri  28112  imsmetlem  28131  vacn  28135  nmcvcn  28136  smcnlem  28138  blometi  28244  ipblnfi  28297  minvecolem2  28317  hhssnv  28707  nmcoplbi  29473  nmopcoi  29540  nmopcoadji  29546  idleop  29576  cdj1i  29878  isoun  30059  xlt2addrd  30102  omndmul  30290  ogrpsub  30293  archirngz  30319  gsumle  30355  ofldchr  30390  lssdimle  30438  pstmxmet  30552  nexple  30683  esumpmono  30753  esumcvg  30760  meascnbl  30894  omsmon  30972  omsmeas  30997  dstfrvinc  31151  hgt750lemd  31342  hgt750lema  31351  hgt750leme  31352  derangenlem  31766  subfaclefac  31771  subfaclim  31783  erdszelem10  31795  sinccvglem  32177  iprodefisum  32235  noextendlt  32425  noextendgt  32426  nosupbnd1  32463  nosupbnd2lem1  32464  unbdqndv2lem2  33097  itg2gt0cn  34084  ibladdnclem  34085  iblabsnc  34093  iblmulc2nc  34094  itgabsnc  34098  bddiblnc  34099  ftc1anclem7  34110  ftc1anclem8  34111  ftc1anc  34112  mettrifi  34171  equivbnd2  34209  heiborlem6  34233  bfplem1  34239  bfp  34241  rrnmet  34246  rrndstprj1  34247  rrndstprj2  34248  dalawlem3  36021  dalawlem4  36022  dalawlem6  36024  dalawlem9  36027  dalawlem11  36029  dalawlem12  36030  dalawlem15  36033  cdleme3c  36378  cdleme7e  36395  cdleme26e  36507  cdleme26eALTN  36509  cdleme27a  36515  cdleme32c  36591  cdleme32e  36593  cdleme32le  36595  cdlemg9b  36781  cdlemg12b  36792  cdlemg12d  36794  trlcolem  36874  trlcone  36876  cdlemk7  36996  cdlemk7u  37018  cdlemk39  37064  cdlemk11ta  37077  cdlemk11tc  37093  mapdcnvatN  37814  irrapxlem5  38342  pell1qrge1  38386  pell1qrgaplem  38389  pell14qrgapw  38392  pellqrex  38395  pellfund14  38414  expmordi  38463  jm2.17a  38478  jm2.17c  38480  acongeq  38501  jm2.19  38511  jm2.27a  38523  jm2.27c  38525  jm3.1lem2  38536  areaquad  38752  rp-isfinite6  38813  hashnzfzclim  39469  binomcxplemnotnn0  39503  absimlere  40607  monoord2xrv  40611  ltmod  40770  dvbdfbdioolem2  41064  ioodvbdlimc1lem2  41067  ioodvbdlimc2lem  41069  stoweidlem3  41139  stoweidlem26  41162  wallispilem1  41201  wallispilem5  41205  stirlinglem1  41210  stirlinglem5  41214  stirlinglem8  41217  stirlinglem10  41219  stirlinglem12  41221  fourierdlem6  41249  fourierdlem7  41250  fourierdlem14  41257  fourierdlem19  41262  fourierdlem35  41278  fourierdlem39  41282  fourierdlem42  41285  fourierdlem50  41292  fourierdlem73  41315  fourierdlem76  41318  fourierdlem77  41319  fourierdlem81  41323  fourierdlem90  41332  fourierdlem92  41334  fourierdlem93  41335  fourierdlem111  41353  fouriersw  41367  etransclem38  41408  sge0split  41542  lighneallem4a  42538  rnghmsubcsetc  42984  rhmsubcsetc  43030  rhmsubcrngc  43036  rhmsubc  43097  rhmsubcALTV  43115  logbpw2m1  43368  dignn0flhalflem1  43416  dignn0flhalflem2  43417  2itscp  43509  amgmwlem  43646