Theorem 3brtr4d 4615

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

Syntax hints:   → wi 4   = wceq 1475   class class class wbr 4583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584

This theorem is referenced by:  f1oiso2  6502  sucdom2  8041  ordtypelem6  8311  cdaen  8878  cdacomen  8886  cdadom1  8891  fin23lem26  9030  distrnq  9662  lediv12a  10795  recp1lt1  10800  ifle  11902  xleadd1a  11955  xlemul1a  11990  fldiv4p1lem1div2  12498  fldiv4lem1div2  12500  quoremz  12516  quoremnn0ALT  12518  intfracq  12520  modmulnn  12550  fzennn  12629  monoord2  12694  expgt1  12760  leexp2r  12780  leexp1a  12781  bernneq  12852  expmulnbnd  12858  digit1  12860  faclbnd  12939  faclbnd4lem3  12944  faclbnd4lem4  12945  faclbnd6  12948  facubnd  12949  hashdomi  13030  fzsdom2  13075  absrele  13896  absimle  13897  abstri  13918  abs2difabs  13922  limsupval2  14059  rlimrege0  14158  rlimrecl  14159  climsqz  14219  climsqz2  14220  rlimdiv  14224  rlimsqz  14228  rlimsqz2  14229  isercolllem1  14243  isercoll2  14247  fsumcvg2  14305  fsumrlim  14384  o1fsum  14386  cvgcmpce  14391  isumle  14415  climcndslem1  14420  climcndslem2  14421  harmonic  14430  expcnv  14435  explecnv  14436  geomulcvg  14446  efcllem  14647  ege2le3  14659  eflegeo  14690  rpnnen2lem4  14785  ruclem2  14800  ruclem8  14805  fsumdvds  14868  phibnd  15314  iserodd  15378  pcdvdstr  15418  pcprmpw2  15424  pockthg  15448  prmreclem4  15461  prmolefac  15588  2expltfac  15637  mod2ile  16929  odsubdvds  17809  pgpfi  17843  fislw  17863  efgredlemd  17980  efgredlem  17983  frgpcpbl  17995  abvres  18662  abvtrivd  18663  znrrg  19733  cstucnd  21898  psmetge0  21927  psmetres2  21929  xmetge0  21959  xmetres2  21976  imasf1oxmet  21990  comet  22128  stdbdxmet  22130  dscmet  22187  nrmmetd  22189  nmrtri  22238  tngngp  22268  nmolb2d  22332  nmoleub  22345  nmoco  22351  nmotri  22353  nmoid  22356  nmods  22358  cnmet  22385  xrsxmet  22420  metdstri  22462  metnrmlem3  22472  lebnumlem3  22570  ipcau2  22841  tchcphlem1  22842  tchcph  22844  trirn  22991  rrxmet  22999  rrxdstprj1  23000  minveclem2  23005  ovolunlem1a  23071  ovolscalem1  23088  volss  23108  voliunlem1  23125  volcn  23180  itg1climres  23287  mbfi1fseqlem5  23292  mbfi1fseqlem6  23293  itg2const2  23314  itg2seq  23315  itg2mulc  23320  itg2splitlem  23321  itg2monolem1  23323  itg2i1fseqle  23327  itg2i1fseq  23328  itg2i1fseq2  23329  itg2addlem  23331  itg2cnlem1  23334  itg2cnlem2  23335  iblss  23377  itgle  23382  ibladdlem  23392  iblabs  23401  iblabsr  23402  iblmulc2  23403  itgabs  23407  bddmulibl  23411  dvfsumabs  23590  dvfsumlem2  23594  dvfsum2  23601  deg1suble  23671  deg1mul3le  23680  plyeq0lem  23770  dgrcolem2  23834  geolim3  23898  aaliou3lem2  23902  aaliou3lem8  23904  ulmdvlem1  23958  radcnvlem1  23971  radcnvlem2  23972  dvradcnv  23979  pserulm  23980  pserdvlem2  23986  abelthlem2  23990  abelthlem5  23993  abelthlem7  23996  abelth2  24000  tangtx  24061  tanabsge  24062  tanord1  24087  argregt0  24160  argrege0  24161  argimgt0  24162  abslogle  24168  logcnlem4  24191  logtayllem  24205  abscxpbnd  24294  ang180lem2  24340  atanlogsublem  24442  atans2  24458  leibpi  24469  birthdaylem3  24480  cxplim  24498  cxp2limlem  24502  cxploglim2  24505  jensenlem2  24514  jensen  24515  amgmlem  24516  emcllem2  24523  emcllem4  24525  emcllem7  24528  zetacvg  24541  lgamgulmlem2  24556  lgamgulmlem5  24559  lgamcvg2  24581  ftalem5  24603  basellem4  24610  basellem6  24612  basellem8  24614  basellem9  24615  chtwordi  24682  chpwordi  24683  ppiwordi  24688  ppiub  24729  vmalelog  24730  chtlepsi  24731  chtleppi  24735  chtublem  24736  chtub  24737  chpub  24745  logfaclbnd  24747  logfacrlim  24749  dchrptlem3  24791  bcmono  24802  bclbnd  24805  bposlem1  24809  bposlem6  24814  bposlem9  24817  lgsqrlem4  24874  2lgslem1c  24918  chebbnd1lem1  24958  chebbnd1lem3  24960  chebbnd1  24961  chtppilimlem1  24962  vmadivsum  24971  rplogsumlem2  24974  dchrisumlema  24977  dchrisumlem3  24980  dchrmusum2  24983  dchrvmasumlem3  24988  dchrvmasumiflem1  24990  dchrisum0flblem1  24997  dchrisum0re  25002  dchrisum0lem2a  25006  mulogsumlem  25020  mulog2sumlem1  25023  mulog2sumlem2  25024  2vmadivsumlem  25029  selberg2lem  25039  selberg3lem1  25046  selberg4lem1  25049  pntrlog2bndlem3  25068  pntrlog2bndlem5  25070  pntrlog2bndlem6  25072  pntpbnd1  25075  pntlemc  25084  pntlemr  25091  pntlemk  25095  pntlemo  25096  abvcxp  25104  ostth2lem1  25107  padicabv  25119  ostth2lem2  25123  ostth2lem3  25124  ostth2lem4  25125  ostth2  25126  legso  25294  trgcopy  25496  nvmtri  26910  imsmetlem  26929  vacn  26933  nmcvcn  26934  smcnlem  26936  blometi  27042  ipblnfi  27095  minvecolem2  27115  hhssnv  27505  nmcoplbi  28271  nmopcoi  28338  nmopcoadji  28344  idleop  28374  cdj1i  28676  isoun  28862  xlt2addrd  28913  omndmul  29045  ogrpsub  29048  archirngz  29074  gsumle  29110  ofldchr  29145  pstmxmet  29268  nexple  29399  esumpmono  29468  esumcvg  29475  meascnbl  29609  omsmon  29687  omsmeas  29712  dstfrvinc  29865  derangenlem  30407  subfaclefac  30412  subfaclim  30424  erdszelem10  30436  sinccvglem  30820  iprodefisum  30880  unbdqndv2lem2  31671  itg2gt0cn  32635  ibladdnclem  32636  iblabsnc  32644  iblmulc2nc  32645  itgabsnc  32649  bddiblnc  32650  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  mettrifi  32723  equivbnd2  32761  heiborlem6  32785  bfplem1  32791  bfp  32793  rrnmet  32798  rrndstprj1  32799  rrndstprj2  32800  dalawlem3  34177  dalawlem4  34178  dalawlem6  34180  dalawlem9  34183  dalawlem11  34185  dalawlem12  34186  dalawlem15  34189  cdleme3c  34535  cdleme7e  34552  cdleme26e  34665  cdleme26eALTN  34667  cdleme27a  34673  cdleme32c  34749  cdleme32e  34751  cdleme32le  34753  cdlemg9b  34939  cdlemg12b  34950  cdlemg12d  34952  trlcolem  35032  trlcone  35034  cdlemk7  35154  cdlemk7u  35176  cdlemk39  35222  cdlemk11ta  35235  cdlemk11tc  35251  mapdcnvatN  35973  irrapxlem5  36408  pell1qrge1  36452  pell1qrgaplem  36455  pell14qrgapw  36458  pellqrex  36461  pellfund14  36480  expmordi  36530  jm2.17a  36545  jm2.17c  36547  acongeq  36568  jm2.19  36578  jm2.27a  36590  jm2.27c  36592  jm3.1lem2  36603  areaquad  36821  rp-isfinite6  36883  hashnzfzclim  37543  binomcxplemnotnn0  37577  ltmod  38705  dvbdfbdioolem2  38819  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  stoweidlem3  38896  stoweidlem26  38919  wallispilem1  38958  wallispilem5  38962  stirlinglem1  38967  stirlinglem5  38971  stirlinglem8  38974  stirlinglem10  38976  stirlinglem12  38978  fourierdlem6  39006  fourierdlem7  39007  fourierdlem14  39014  fourierdlem19  39019  fourierdlem35  39035  fourierdlem39  39039  fourierdlem42  39042  fourierdlem50  39049  fourierdlem73  39072  fourierdlem76  39075  fourierdlem77  39076  fourierdlem81  39080  fourierdlem90  39089  fourierdlem92  39091  fourierdlem93  39092  fourierdlem111  39110  fouriersw  39124  etransclem38  39165  sge0split  39302  lighneallem4a  40063  eucrct2eupth  41413  rnghmsubcsetc  41769  rhmsubcsetc  41815  rhmsubcrngc  41821  rhmsubc  41882  rhmsubcALTV  41901  logbpw2m1  42159  dignn0flhalflem1  42207  dignn0flhalflem2  42208  amgmwlem  42357