Theorem eqbrtrd 4605

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 8-Oct-1999.)

Hypotheses

Ref	Expression
eqbrtrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqbrtrd.2	⊢ (𝜑 → 𝐵𝑅𝐶)

Assertion

Ref	Expression
eqbrtrd	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem eqbrtrd

Step	Hyp	Ref	Expression
1		eqbrtrd.2	. 2 ⊢ (𝜑 → 𝐵𝑅𝐶)
2		eqbrtrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	2	breq1d 4593	. 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
4	1, 3	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:  eqbrtrrd  4607  somin2  5450  en1b  7910  domunsncan  7945  fodomfi  8124  hartogslem1  8330  wemaplem2  8335  infdifsn  8437  carddomi2  8679  cdaun  8877  cda1dif  8881  mapcdaen  8889  cdaxpdom  8894  cdafi  8895  cdainf  8897  carden  9252  alephsuc3  9281  fpwwe2lem6  9336  fpwwe2lem7  9337  inar1  9476  rankcf  9478  lesub3d  10524  lbinfle  10857  supadd  10868  supmul  10872  rpnnen1lem3  11692  rpnnen1lem3OLD  11698  divge1  11774  xrmin1  11882  xrmin2  11883  ifle  11902  qbtwnxr  11905  xltnegi  11921  xleadd1a  11955  xlt2add  11962  xlemul1a  11990  xov1plusxeqvd  12189  ubmelm1fzo  12430  flflp1  12470  ceim1l  12508  ceilm1lt  12509  ceille  12511  quoremz  12516  quoremnn0ALT  12518  modlt  12541  modeqmodmin  12602  addmodlteq  12607  seqf1olem1  12702  bernneq  12852  discr  12863  faclbnd2  12940  faclbnd4lem3  12944  hashun2  13033  hashfun  13084  ccatsymb  13219  ccatrn  13225  sqrlem6  13836  sqrlem7  13837  rddif  13928  amgm2  13957  icodiamlt  14022  climconst  14122  rlimconst  14123  serclim0  14156  rlimcn1  14167  mulcn2  14174  reccn2  14175  o1mul  14193  o1rlimmul  14197  iserex  14235  climlec2  14237  iserge0  14239  climcau  14249  caucvgrlem  14251  caucvgr  14254  iseraltlem2  14261  iseraltlem3  14262  iseralt  14263  fsumabs  14374  o1fsum  14386  iserabs  14388  climfsum  14393  isumless  14416  climcndslem2  14421  divrcnv  14423  flo1  14425  supcvg  14427  georeclim  14442  geomulcvg  14446  cvgrat  14454  mertenslem1  14455  prodfclim1  14464  fprodge1  14565  fprodle  14566  efcvgfsum  14655  eftlub  14678  eflegeo  14690  tanhlt1  14729  tanhbnd  14730  ef01bndlem  14753  sin01bnd  14754  cos01bnd  14755  cos01gt0  14760  ruclem2  14800  ruclem3  14801  ruclem9  14806  ruclem11  14808  ruclem12  14809  bitsfzolem  14994  bitsfzo  14995  bitsinv1lem  15001  sadcaddlem  15017  mulgcd  15103  eucalglt  15136  lcmledvds  15150  lcmfledvds  15183  mulgcddvds  15207  coprmproddvdslem  15214  prmind2  15236  isprm5  15257  divdenle  15295  nonsq  15305  pythagtriplem4  15362  pclem  15381  pcpremul  15386  pczdvds  15405  pcprmpw2  15424  qexpz  15443  prmreclem4  15461  prmreclem5  15462  4sqlem10  15489  ramtub  15554  ramub2  15556  prmodvdslcmf  15589  prmgaplem8  15600  natpropd  16459  catciso  16580  p0le  16866  acsdomd  17004  qusgrp  17472  f1otrspeq  17690  pmtrfrn  17701  pmtrfconj  17709  symggen  17713  psgnunilem4  17740  oddvds2  17806  odcau  17842  pgpfi  17843  pgpssslw  17852  sylow3lem4  17868  efgred2  17989  frgp0  17996  odadd2  18075  oddvdssubg  18081  ablfac1c  18293  ablfac1eu  18295  pgpfaclem3  18305  isabvd  18643  abvsubtri  18658  mplsubrg  19261  coe1sfi  19404  cyggic  19740  mp2pm2mplem5  20434  en2top  20600  1stcrest  21066  2ndcrest  21067  hausmapdom  21113  ufilen  21544  xmetrtri2  21971  prdsxmetlem  21983  bl2in  22015  xblcntrps  22025  xblcntr  22026  ssblps  22037  ssbl  22038  blssps  22039  blss  22040  blcld  22120  methaus  22135  metustexhalf  22171  nmtri2  22241  tngngp3  22270  nrginvrcnlem  22305  nrginvrcn  22306  nmoi  22342  nmo0  22349  nmoid  22356  blcvx  22409  reperflem  22429  reconnlem2  22438  metdcnlem  22447  metdscn  22467  metnrmlem3  22472  mulc1cncf  22516  iccpnfhmeo  22552  cnheiborlem  22561  cnheibor  22562  lebnumii  22573  pcopt  22630  pcopt2  22631  pcoass  22632  nmoleub2lem  22722  nmoleub2lem3  22723  nmoleub2lem2  22724  ipcau2  22841  tchcphlem1  22842  nglmle  22908  trirn  22991  rrxdstprj1  23000  minveclem3  23008  ivthlem2  23028  ivthlem3  23029  ivth2  23031  ovollb  23054  ovolsslem  23059  ovollb2lem  23063  ovolctb  23065  ovoliunlem1  23077  ovolsca  23090  ovolicc1  23091  ovolicc2lem4  23095  nulmbl  23110  ioombl1lem4  23136  uniioovol  23153  uniioombllem3a  23158  uniioombllem4  23160  opnmbllem  23175  volcn  23180  volivth  23181  i1fadd  23268  i1fmul  23269  mbfi1fseqlem4  23291  mbfi1fseqlem5  23292  mbfi1fseqlem6  23293  itg2const2  23314  itg2seq  23315  itg2uba  23316  itg2split  23322  itg2monolem1  23323  itg2monolem3  23325  itg2i1fseq2  23329  itg2addlem  23331  itg2gt0  23333  itg2cnlem1  23334  itg2cnlem2  23335  itgless  23389  ibladdlem  23392  bddmulibl  23411  dveflem  23546  dvferm1lem  23551  dvferm2lem  23553  dvlip  23560  dvlipcn  23561  dvlip2  23562  dvle  23574  dvivthlem1  23575  lhop1lem  23580  dvcvx  23587  dvfsumabs  23590  dvfsumlem2  23594  dvfsumlem4  23596  dvfsumrlim2  23599  dvfsum2  23601  ftc1a  23604  ftc1lem4  23606  ftc1lem5  23607  deg1sub  23672  ply1divex  23700  deg1submon1p  23716  r1pdeglt  23722  dvdsq1p  23724  fta1glem2  23730  fta1g  23731  plyeq0lem  23770  dgrlt  23826  fta1lem  23866  aalioulem2  23892  aalioulem3  23893  aalioulem4  23894  aaliou3lem2  23902  aaliou3lem9  23909  taylply2  23926  ulmbdd  23956  ulmdvlem1  23958  mtest  23962  mtestbdd  23963  radcnvlem1  23971  radcnvle  23978  pserulm  23980  psercn  23984  pserdvlem2  23986  abelthlem2  23990  abelthlem5  23993  abelthlem7  23996  abelthlem8  23997  abelthlem9  23998  reeff1olem  24004  tangtx  24061  tanord  24088  efif1olem4  24095  logrnaddcl  24125  logcj  24156  logimul  24164  logneg2  24165  logdivlti  24170  divlogrlim  24181  logcnlem3  24190  logcnlem4  24191  efopn  24204  logtayllem  24205  logtayl  24206  cxpcn3lem  24288  cxpaddle  24293  abscxpbnd  24294  asinlem3  24398  asinneg  24413  asinsin  24419  atanlogaddlem  24440  atantan  24450  bndatandm  24456  atans2  24458  atantayl  24464  atantayl2  24465  atantayl3  24466  leibpi  24469  birthdaylem3  24480  rlimcnp  24492  efrlim  24496  cxplim  24498  cxp2lim  24503  cxploglim2  24505  divsqrtsumo1  24510  jensenlem2  24514  amgm  24517  logdifbnd  24520  harmonicbnd4  24537  fsumharmonic  24538  lgamgulmlem2  24556  lgamgulmlem3  24557  lgamgulmlem5  24559  lgambdd  24563  lgamcvg2  24581  ftalem1  24599  ftalem5  24603  basellem1  24607  basellem8  24614  ppip1le  24687  ppiltx  24703  sqff1o  24708  chtublem  24736  chpub  24745  logfaclbnd  24747  logfacrlim  24749  logexprlim  24750  mersenne  24752  bcmono  24802  bcmax  24803  bposlem2  24810  bposlem5  24813  lgslem3  24824  gausslemma2dlem1a  24890  lgsquadlem1  24905  lgsquadlem2  24906  2lgslem1c  24918  2sqblem  24956  chebbnd1  24961  chtppilimlem1  24962  chto1ub  24965  chpchtlim  24968  chpo1ubb  24970  rplogsumlem1  24973  rplogsumlem2  24974  rpvmasumlem  24976  dchrisumlem1  24978  dchrisumlem2  24979  dchrmusum2  24983  dchrvmasumlem2  24987  dchrvmasumlem3  24988  dchrvmasumiflem1  24990  dchrisum0flblem1  24997  dchrisum0fno1  25000  dchrisum0lem1b  25004  dchrisum0lem1  25005  dchrisum0lem2a  25006  dchrisum0lem2  25007  rplogsum  25016  mudivsum  25019  mulogsumlem  25020  mulog2sumlem1  25023  mulog2sumlem2  25024  vmalogdivsum2  25027  2vmadivsumlem  25029  selberglem2  25035  selberg2b  25041  logdivbnd  25045  selberg3lem1  25046  selberg3lem2  25047  selberg4lem1  25049  pntrmax  25053  pntrsumo1  25054  pntrlog2bndlem1  25066  pntrlog2bndlem2  25067  pntrlog2bndlem3  25068  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  pntrlog2bnd  25073  pntpbnd1a  25074  pntpbnd2  25076  pntibndlem2  25080  pntlemb  25086  pntlemg  25087  pntlemh  25088  pntlemr  25091  pntlemj  25092  pntlemf  25094  pntlemo  25096  pnt  25103  padicabv  25119  ostth2lem2  25123  ostth2lem3  25124  ostth3  25127  colperpexlem3  25424  mideulem2  25426  lnperpex  25495  trgcopy  25496  iscgra1  25502  brbtwn2  25585  colinearalglem4  25589  nvabs  26911  nvge0  26912  smcnlem  26936  nmblolbii  27038  blocnilem  27043  siii  27092  ubthlem2  27111  minvecolem3  27116  htthlem  27158  bcsiALT  27420  bcs3  27424  chscllem4  27883  0cnop  28222  0cnfn  28223  nmbdoplbi  28267  nmcoplbi  28271  nmophmi  28274  nmbdfnlbi  28292  nmcfnlbi  28295  nlelchi  28304  riesz1  28308  cnlnadjlem2  28311  nmopadjlei  28331  nmoptrii  28337  nmopcoi  28338  nmopcoadji  28344  unierri  28347  branmfn  28348  pjs14i  28453  hstle  28473  cdj3lem2b  28680  xlt2addrd  28913  eliccelico  28929  elicoelioo  28930  ltesubnnd  28955  archirngz  29074  archiabllem2c  29080  madjusmdetlem2  29222  locfinref  29236  sqsscirc1  29282  tpr2rico  29286  esumcst  29452  esumgect  29479  esum2d  29482  measunl  29606  measiun  29608  omssubaddlem  29688  omssubadd  29689  carsgsigalem  29704  carsgclctunlem2  29708  pmeasmono  29713  eulerpartlemgc  29751  eulerpartlemb  29757  ballotlemsel1i  29901  ballotlemro  29911  sgnsub  29933  signsplypnf  29953  signsply0  29954  signsvtn  29987  signsvfnn  29989  erdsze2lem1  30439  sinccvglem  30820  divcnvlin  30871  iprodefisum  30880  faclimlem2  30883  nodense  31088  nobnddown  31100  fnemeet1  31531  dnibndlem10  31647  dnibndlem11  31648  dnibnd  31651  knoppcnlem4  31656  knoppcnlem6  31658  unblimceq0lem  31667  unblimceq0  31668  unbdqndv2lem1  31670  unbdqndv2lem2  31671  knoppndvlem11  31683  knoppndvlem12  31684  knoppndvlem14  31686  knoppndvlem15  31687  knoppndvlem17  31689  knoppndvlem18  31690  knoppndvlem19  31691  knoppndvlem21  31693  ltflcei  32567  ptrecube  32579  poimirlem16  32595  poimirlem17  32596  poimirlem29  32608  broucube  32613  opnmbllem0  32615  mblfinlem2  32617  mblfinlem3  32618  ismblfin  32620  itg2addnclem  32631  itg2addnclem2  32632  itg2addnclem3  32633  itg2addnc  32634  ibladdnclem  32636  ftc1cnnclem  32653  ftc1cnnc  32654  ftc1anc  32663  geomcau  32725  prdsbnd  32762  cntotbnd  32765  heiborlem4  32783  rrndstprj2  32800  rrncmslem  32801  rrnequiv  32804  iccbnd  32809  cvlcvr1  33644  cvrat3  33746  dalem25  34002  cdlema1N  34095  dalawlem3  34177  dalawlem4  34178  dalawlem5  34179  dalawlem6  34180  dalawlem7  34181  dalawlem9  34183  dalawlem11  34185  dalawlem12  34186  lhp2lt  34305  lhpmcvr  34327  4atexlemcnd  34376  lautj  34397  trlle  34489  trlval3  34492  trlval4  34493  cdleme0moN  34530  cdleme13  34577  cdleme15  34583  cdleme19b  34610  cdleme20e  34619  cdleme20j  34624  cdleme22e  34650  cdleme22eALTN  34651  cdleme26fALTN  34668  cdleme26f  34669  cdleme27N  34675  cdleme41sn3a  34739  cdleme46fsvlpq  34811  cdlemeg46vrg  34833  cdlemg4  34923  cdlemg7N  34932  cdlemg9a  34938  cdlemg11b  34948  cdlemg12a  34949  trljco  35046  tendoidcl  35075  tendococl  35078  tendopltp  35086  tendo0tp  35095  tendoicl  35102  cdlemi2  35125  cdlemk5a  35141  cdlemk5  35142  cdlemk12  35156  cdlemkole  35159  cdlemk14  35160  cdlemk12u  35178  cdlemk37  35220  cdlemk39s-id  35246  cdlemk49  35257  cdlemk39u1  35273  cdlemk39u  35274  dian0  35346  cdlemm10N  35425  cdlemn2  35502  cdlemn10  35513  dihord1  35525  dihord10  35530  dihmeetlem4preN  35613  dihmeetlem18N  35631  dihmeetlem20N  35633  dihjatc  35724  mapdcnvatN  35973  lzenom  36351  irrapxlem2  36405  irrapxlem3  36406  irrapxlem5  36408  pellexlem2  36412  pell14qrgt0  36441  pellfundlb  36466  pellfundex  36468  pellfund14  36480  rmspecsqrtnq  36488  rmspecsqrtnqOLD  36489  jm2.24nn  36544  jm2.17a  36545  jm2.17b  36546  congabseq  36559  acongrep  36565  acongeq  36568  jm2.26lem3  36586  jm2.27a  36590  jm2.27c  36592  hbtlem2  36713  dgraaub  36737  idomodle  36793  relexpxpmin  37028  frege102d  37065  hashnzfzclim  37543  binomcxplemfrat  37572  binomcxplemnotnn0  37577  suprnmpt  38350  mpct  38388  dstregt0  38434  lefldiveq  38446  fzisoeu  38455  upbdrech  38460  ssfiunibd  38464  fzdifsuc2  38466  xadd0ge  38477  supxrgere  38490  supxrge  38495  suplesup  38496  xrlexaddrp  38509  infxrunb2  38525  infleinflem2  38528  reclt0d  38548  ioondisj2  38561  iccshift  38591  iooshift  38595  fmul01  38647  fmul01lt1lem1  38651  fmul01lt1lem2  38652  climrec  38670  climsuse  38675  mullimc  38683  mullimcf  38690  constlimc  38691  idlimc  38693  divcnvg  38694  limcperiod  38695  limcrecl  38696  lptioo2  38698  lptioo1  38699  islpcn  38706  lptre2pt  38707  limcleqr  38711  neglimc  38714  addlimc  38715  0ellimcdiv  38716  limclner  38718  climleltrp  38743  sinaover2ne0  38751  cncfshift  38759  cncfperiod  38764  cncfioobdlem  38782  cncfioobd  38783  fperdvper  38808  dvdivbd  38813  dvbdfbdioolem1  38818  dvbdfbdioolem2  38819  ioodvbdlimc1lem1  38821  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvnmul  38833  dvnprodlem1  38836  itgiccshift  38872  itgperiod  38873  ismbl3  38879  ovolsplit  38881  stoweidlem1  38894  stoweidlem11  38904  stoweidlem13  38906  stoweidlem14  38907  stoweidlem16  38909  stoweidlem21  38914  stoweidlem25  38918  stoweidlem26  38919  stoweidlem36  38929  stoweidlem38  38931  stoweidlem41  38934  stoweidlem42  38935  stoweidlem45  38938  stoweidlem48  38941  stoweidlem52  38945  stoweidlem62  38955  wallispilem3  38960  stirlinglem5  38971  stirlinglem6  38972  stirlinglem7  38973  stirlinglem10  38976  stirlinglem12  38978  stirlinglem15  38981  dirkercncflem1  38996  fourierdlem10  39010  fourierdlem12  39012  fourierdlem15  39015  fourierdlem16  39016  fourierdlem19  39019  fourierdlem20  39020  fourierdlem21  39021  fourierdlem22  39022  fourierdlem24  39024  fourierdlem30  39030  fourierdlem37  39037  fourierdlem39  39039  fourierdlem40  39040  fourierdlem41  39041  fourierdlem42  39042  fourierdlem47  39046  fourierdlem48  39047  fourierdlem49  39048  fourierdlem50  39049  fourierdlem52  39051  fourierdlem54  39053  fourierdlem60  39059  fourierdlem61  39060  fourierdlem63  39062  fourierdlem64  39063  fourierdlem68  39067  fourierdlem71  39070  fourierdlem72  39071  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem77  39076  fourierdlem78  39077  fourierdlem79  39078  fourierdlem81  39080  fourierdlem82  39081  fourierdlem83  39082  fourierdlem84  39083  fourierdlem87  39086  fourierdlem92  39091  fourierdlem93  39092  fourierdlem94  39093  fourierdlem101  39100  fourierdlem102  39101  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  fourierdlem112  39111  fourierdlem113  39112  fourierdlem114  39113  sqwvfoura  39121  sqwvfourb  39122  fouriersw  39124  elaa2lem  39126  etransclem23  39150  etransclem28  39155  etransclem32  39159  etransclem35  39162  etransclem48  39175  qndenserrnbllem  39190  rrnprjdstle  39197  ioorrnopnlem  39200  ioorrnopnxrlem  39202  salexct  39228  sge0fsum  39280  sge0supre  39282  sge0rnbnd  39286  sge0lefi  39291  sge0lessmpt  39292  sge0ltfirp  39293  sge0prle  39294  sge0resrnlem  39296  sge0le  39300  sge0split  39302  sge0iunmptlemre  39308  sge0iunmpt  39311  sge0isum  39320  sge0xaddlem1  39326  sge0xaddlem2  39327  sge0xadd  39328  sge0reuz  39340  sge0reuzb  39341  meaunle  39357  meaiunlelem  39361  voliunsge0lem  39365  meaiuninc  39374  meaiininclem  39376  omeunle  39406  omeiunle  39407  omelesplit  39408  omeiunltfirp  39409  carageniuncllem2  39412  caratheodorylem2  39417  caragencmpl  39425  ovnlecvr  39448  ovncvrrp  39454  ovnsubaddlem1  39460  ovnsubadd  39462  hoidmv1lelem1  39481  hoidmv1lelem2  39482  hoidmv1le  39484  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem5  39489  hoidmvle  39490  ovnhoilem1  39491  ovnlecvr2  39500  ovncvr2  39501  hoiqssbllem2  39513  hspmbllem2  39517  hspmbllem3  39518  ovnsplit  39538  ovolval5lem1  39542  vonioolem1  39571  vonioolem2  39572  vonicclem1  39574  vonicclem2  39575  pimconstlt1  39592  smflimlem2  39658  smflimlem4  39660  smfmullem1  39676  iccpartltu  39963  iccpartleu  39966  subupgr  40511  crctcsh1wlkn0lem1  41013  pgrple2abl  41940  difmodm1lt  42111  nnpw2blen  42172  dignn0flhalflem1  42207