Theorem eqbrtrd 5170

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 5158	. 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
4	1, 3	mpbird 257	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149

This theorem is referenced by:  eqbrtrrd  5172  somin2  6134  en1b  9020  en1bOLD  9021  domunsncan  9069  fodomfi  9322  infsupprpr  9496  hartogslem1  9534  wemaplem2  9539  infdifsn  9649  ttrclselem2  9718  carddomi2  9962  djuinf  10180  carden  10543  alephsuc3  10572  fpwwe2lem5  10627  fpwwe2lem6  10628  inar1  10767  rankcf  10769  lesub3d  11829  lbinfle  12166  supadd  12179  supmul  12183  rpnnen1lem3  12960  divge1  13039  xrmin1  13153  xrmin2  13154  ifle  13173  qbtwnxr  13176  xltnegi  13192  xleadd1a  13229  xlt2add  13236  xlemul1a  13264  xov1plusxeqvd  13472  ubmelm1fzo  13725  flflp1  13769  ceim1l  13809  ceilm1lt  13810  ceille  13812  quoremz  13817  quoremnn0ALT  13819  modlt  13842  modeqmodmin  13903  addmodlteq  13908  seqf1olem1  14004  bernneq  14189  discr  14200  faclbnd2  14248  faclbnd4lem3  14252  hashun2  14340  hashfun  14394  ccatsymb  14529  ccatrn  14536  01sqrexlem6  15191  01sqrexlem7  15192  rddif  15284  amgm2  15313  icodiamlt  15379  climconst  15484  rlimconst  15485  serclim0  15518  rlimcn1  15529  mulcn2  15537  reccn2  15538  o1mul  15556  o1rlimmul  15560  iserex  15600  climlec2  15602  iserge0  15604  climcau  15614  caucvgrlem  15616  caucvgr  15619  iseraltlem2  15626  iseraltlem3  15627  iseralt  15628  fsumabs  15744  o1fsum  15756  iserabs  15758  climfsum  15763  isumless  15788  climcndslem2  15793  divrcnv  15795  flo1  15797  supcvg  15799  georeclim  15815  geomulcvg  15819  cvgrat  15826  mertenslem1  15827  prodfclim1  15836  fprodle  15937  efcvgfsum  16026  eftlub  16049  eflegeo  16061  tanhlt1  16100  tanhbnd  16101  ef01bndlem  16124  sin01bnd  16125  cos01bnd  16126  cos01gt0  16131  ruclem2  16172  ruclem3  16173  ruclem9  16178  ruclem11  16180  ruclem12  16181  bitsfzolem  16372  bitsfzo  16373  bitsinv1lem  16379  sadcaddlem  16395  mulgcd  16487  eucalglt  16519  lcmledvds  16533  lcmfledvds  16566  mulgcddvds  16589  coprmproddvdslem  16596  prmind2  16619  isprm5  16641  divdenle  16682  nonsq  16692  pythagtriplem4  16749  pclem  16768  pcpremul  16773  pczdvds  16793  pcprmpw2  16812  qexpz  16831  prmreclem4  16849  prmreclem5  16850  4sqlem10  16877  ramtub  16942  ramub2  16944  prmodvdslcmf  16977  prmgaplem8  16988  natpropd  17926  catciso  18058  p0le  18379  acsdomd  18507  triv1nsgd  19048  qusgrp  19060  f1otrspeq  19310  pmtrfrn  19321  pmtrfconj  19329  symggen  19333  psgnunilem4  19360  oddvds2  19429  odcau  19467  pgpfi  19468  pgpssslw  19477  sylow3lem4  19493  efgred2  19616  frgp0  19623  odadd2  19712  oddvdssubg  19718  ablfac1c  19936  ablfac1eu  19938  pgpfaclem3  19948  2nsgsimpgd  19967  isabvd  20421  abvsubtri  20436  cyggic  21120  mplsubrg  21556  coe1sfi  21729  mp2pm2mplem5  22304  en2top  22480  1stcrest  22949  2ndcrest  22950  hausmapdom  22996  ufilen  23426  xmetrtri2  23854  prdsxmetlem  23866  bl2in  23898  xblcntrps  23908  xblcntr  23909  ssblps  23920  ssbl  23921  blssps  23922  blss  23923  blcld  24006  methaus  24021  metustexhalf  24057  nmtri2  24128  tngngp3  24165  nrginvrcnlem  24200  nrginvrcn  24201  nmoi  24237  nmo0  24244  nmoid  24251  blcvx  24306  reperflem  24326  reconnlem2  24335  metdcnlem  24344  metdscn  24364  metnrmlem3  24369  mulc1cncf  24413  iccpnfhmeo  24453  cnheiborlem  24462  cnheibor  24463  lebnumii  24474  pcopt  24530  pcopt2  24531  pcoass  24532  nmoleub2lem  24622  nmoleub2lem3  24623  nmoleub2lem2  24624  ipcau2  24743  tcphcphlem1  24744  nglmle  24811  trirn  24909  rrxdstprj1  24918  minveclem3  24938  ivthlem2  24961  ivthlem3  24962  ivth2  24964  ovollb  24988  ovolsslem  24993  ovollb2lem  24997  ovolctb  24999  ovoliunlem1  25011  ovolsca  25024  ovolicc1  25025  ovolicc2lem4  25029  nulmbl  25044  ioombl1lem4  25070  uniioovol  25088  uniioombllem3a  25093  uniioombllem4  25095  opnmbllem  25110  volcn  25115  volivth  25116  i1fadd  25204  i1fmul  25205  mbfi1fseqlem4  25228  mbfi1fseqlem5  25229  mbfi1fseqlem6  25230  itg2const2  25251  itg2seq  25252  itg2uba  25253  itg2split  25259  itg2monolem1  25260  itg2monolem3  25262  itg2i1fseq2  25266  itg2addlem  25268  itg2gt0  25270  itg2cnlem1  25271  itg2cnlem2  25272  itgless  25326  ibladdlem  25329  bddmulibl  25348  dveflem  25488  dvferm1lem  25493  dvferm2lem  25495  dvlip  25502  dvlipcn  25503  dvlip2  25504  dvle  25516  dvivthlem1  25517  lhop1lem  25522  dvcvx  25529  dvfsumabs  25532  dvfsumlem2  25536  dvfsumlem4  25538  dvfsumrlim2  25541  dvfsum2  25543  ftc1a  25546  ftc1lem4  25548  ftc1lem5  25549  deg1sub  25618  ply1divex  25646  deg1submon1p  25662  r1pdeglt  25668  dvdsq1p  25670  fta1glem2  25676  fta1g  25677  plyeq0lem  25716  dgrlt  25772  fta1lem  25812  aalioulem2  25838  aalioulem3  25839  aalioulem4  25840  aaliou3lem2  25848  aaliou3lem9  25855  taylply2  25872  ulmbdd  25902  ulmdvlem1  25904  mtest  25908  mtestbdd  25909  radcnvlem1  25917  radcnvle  25924  pserulm  25926  psercn  25930  pserdvlem2  25932  abelthlem2  25936  abelthlem5  25939  abelthlem7  25942  abelthlem8  25943  abelthlem9  25944  reeff1olem  25950  tangtx  26007  tanord  26039  efif1olem4  26046  logrnaddcl  26075  logcj  26106  logimul  26114  logneg2  26115  logdivlti  26120  divlogrlim  26135  logcnlem3  26144  logcnlem4  26145  efopn  26158  logtayllem  26159  logtayl  26160  cxpcn3lem  26245  cxpaddle  26250  abscxpbnd  26251  asinlem3  26366  asinneg  26381  asinsin  26387  atanlogaddlem  26408  atantan  26418  bndatandm  26424  atans2  26426  atantayl  26432  atantayl2  26433  atantayl3  26434  leibpi  26437  birthdaylem3  26448  rlimcnp  26460  efrlim  26464  cxplim  26466  cxp2lim  26471  cxploglim2  26473  divsqrtsumo1  26478  jensenlem2  26482  amgm  26485  logdifbnd  26488  harmonicbnd4  26505  fsumharmonic  26506  lgamgulmlem2  26524  lgamgulmlem3  26525  lgamgulmlem5  26527  lgambdd  26531  lgamcvg2  26549  ftalem1  26567  ftalem5  26571  basellem1  26575  basellem8  26582  ppip1le  26655  ppiltx  26671  sqff1o  26676  chtublem  26704  chpub  26713  logfaclbnd  26715  logfacrlim  26717  logexprlim  26718  mersenne  26720  bcmono  26770  bcmax  26771  bposlem2  26778  bposlem5  26781  lgslem3  26792  gausslemma2dlem1a  26858  lgsquadlem1  26873  lgsquadlem2  26874  2lgslem1c  26886  2sqblem  26924  chebbnd1  26965  chtppilimlem1  26966  chto1ub  26969  chpchtlim  26972  chpo1ubb  26974  rplogsumlem1  26977  rplogsumlem2  26978  rpvmasumlem  26980  dchrisumlem1  26982  dchrisumlem2  26983  dchrmusum2  26987  dchrvmasumlem2  26991  dchrvmasumlem3  26992  dchrvmasumiflem1  26994  dchrisum0flblem1  27001  dchrisum0fno1  27004  dchrisum0lem1b  27008  dchrisum0lem1  27009  dchrisum0lem2a  27010  dchrisum0lem2  27011  rplogsum  27020  mudivsum  27023  mulogsumlem  27024  mulog2sumlem1  27027  mulog2sumlem2  27028  vmalogdivsum2  27031  2vmadivsumlem  27033  selberglem2  27039  selberg2b  27045  logdivbnd  27049  selberg3lem1  27050  selberg3lem2  27051  selberg4lem1  27053  pntrmax  27057  pntrsumo1  27058  pntrlog2bndlem1  27070  pntrlog2bndlem2  27071  pntrlog2bndlem3  27072  pntrlog2bndlem4  27073  pntrlog2bndlem5  27074  pntrlog2bnd  27077  pntpbnd1a  27078  pntpbnd2  27080  pntibndlem2  27084  pntlemb  27090  pntlemg  27091  pntlemh  27092  pntlemr  27095  pntlemj  27096  pntlemf  27098  pntlemo  27100  pnt  27107  padicabv  27123  ostth2lem2  27127  ostth2lem3  27128  ostth3  27131  nosep1o  27174  nodense  27185  noinfbnd2lem1  27223  noetainflem3  27232  mins1  27260  mins2  27261  cofcutr  27401  cofcutrtime  27404  addsuniflem  27474  negsunif  27519  ssltmul1  27592  mulsuniflem  27594  precsexlem11  27653  colperpexlem3  27973  mideulem2  27975  lnperpex  28044  trgcopy  28045  iscgra1  28051  brbtwn2  28153  colinearalglem4  28157  subupgr  28534  crctcshwlkn0lem1  29054  nvabs  29913  nvge0  29914  smcnlem  29938  nmblolbii  30040  blocnilem  30045  siii  30094  ubthlem2  30112  minvecolem3  30117  htthlem  30158  bcsiALT  30420  bcs3  30424  chscllem4  30881  0cnop  31220  0cnfn  31221  nmbdoplbi  31265  nmcoplbi  31269  nmophmi  31272  nmbdfnlbi  31290  nmcfnlbi  31293  nlelchi  31302  riesz1  31306  cnlnadjlem2  31309  nmopadjlei  31329  nmoptrii  31335  nmopcoi  31336  nmopcoadji  31342  unierri  31345  branmfn  31346  pjs14i  31451  hstle  31471  cdj3lem2b  31678  xlt2addrd  31959  eliccelico  31976  elicoelioo  31977  ltesubnnd  32016  wrdt2ind  32105  archirngz  32323  archiabllem2c  32329  ply1degltel  32655  ig1pmindeg  32660  ply1degltdimlem  32696  minplyirredlem  32758  madjusmdetlem2  32797  locfinref  32810  sqsscirc1  32877  tpr2rico  32881  esumcst  33050  esumgect  33077  esum2d  33080  measunl  33203  measiun  33205  omssubaddlem  33287  omssubadd  33288  carsgsigalem  33303  carsgclctunlem2  33307  pmeasmono  33312  eulerpartlemgc  33350  eulerpartlemb  33356  ballotlemsel1i  33500  ballotlemro  33510  sgnsub  33532  signsplypnf  33550  signsply0  33551  signsvtn  33584  signsvfnn  33586  hgt750lemd  33649  logdivsqrle  33651  hashf1dmcdm  34094  erdsze2lem1  34183  sinccvglem  34646  divcnvlin  34691  iprodefisum  34700  faclimlem2  34703  gg-dvfsumlem2  35172  fnemeet1  35240  dnibndlem10  35352  dnibndlem11  35353  dnibnd  35356  knoppcnlem4  35361  knoppcnlem6  35363  unblimceq0lem  35371  unbdqndv2lem1  35374  unbdqndv2lem2  35375  knoppndvlem11  35387  knoppndvlem12  35388  knoppndvlem14  35390  knoppndvlem15  35391  knoppndvlem17  35393  knoppndvlem18  35394  knoppndvlem19  35395  knoppndvlem21  35397  ctbssinf  36276  ltflcei  36465  ptrecube  36477  poimirlem16  36493  poimirlem17  36494  poimirlem29  36506  broucube  36511  opnmbllem0  36513  mblfinlem2  36515  mblfinlem3  36516  ismblfin  36518  itg2addnclem  36528  itg2addnclem2  36529  itg2addnclem3  36530  itg2addnc  36531  ibladdnclem  36533  ftc1cnnclem  36548  ftc1cnnc  36549  ftc1anc  36558  geomcau  36616  prdsbnd  36650  cntotbnd  36653  heiborlem4  36671  rrndstprj2  36688  rrncmslem  36689  rrnequiv  36692  iccbnd  36697  cvlcvr1  38198  cvrat3  38302  dalem25  38558  cdlema1N  38651  dalawlem3  38733  dalawlem4  38734  dalawlem5  38735  dalawlem6  38736  dalawlem7  38737  dalawlem9  38739  dalawlem11  38741  dalawlem12  38742  lhp2lt  38861  lhpmcvr  38883  4atexlemcnd  38932  lautj  38953  trlle  39044  trlval3  39047  trlval4  39048  cdleme0moN  39085  cdleme13  39132  cdleme15  39138  cdleme19b  39164  cdleme20e  39173  cdleme20j  39178  cdleme22e  39204  cdleme22eALTN  39205  cdleme26fALTN  39222  cdleme26f  39223  cdleme27N  39229  cdleme41sn3a  39293  cdleme46fsvlpq  39365  cdlemeg46vrg  39387  cdlemg4  39477  cdlemg7N  39486  cdlemg9a  39492  cdlemg11b  39502  cdlemg12a  39503  trljco  39600  tendoidcl  39629  tendococl  39632  tendopltp  39640  tendo0tp  39649  tendoicl  39656  cdlemi2  39679  cdlemk5a  39695  cdlemk5  39696  cdlemk12  39710  cdlemkole  39713  cdlemk14  39714  cdlemk12u  39732  cdlemk37  39774  cdlemk39s-id  39800  cdlemk49  39811  cdlemk39u1  39827  cdlemk39u  39828  dian0  39899  cdlemm10N  39978  cdlemn2  40055  cdlemn10  40066  dihord1  40078  dihord10  40083  dihmeetlem4preN  40166  dihmeetlem18N  40184  dihmeetlem20N  40186  dihjatc  40277  mapdcnvatN  40526  lcmineqlem17  40899  3lexlogpow5ineq2  40909  3lexlogpow2ineq2  40913  3lexlogpow5ineq5  40914  aks4d1p1p3  40923  aks4d1p1p2  40924  aks4d1p1p4  40925  aks4d1p1p7  40928  aks4d1p1p5  40929  aks4d1p1  40930  aks4d1p3  40932  aks4d1p5  40934  aks4d1p6  40935  aks4d1p7d1  40936  aks4d1p7  40937  aks4d1p8  40941  2ap1caineq  40950  sticksstones7  40957  sticksstones10  40960  sticksstones11  40961  sticksstones12a  40962  sticksstones12  40963  sticksstones22  40973  metakunt16  40989  metakunt29  41002  evlselv  41157  fltltc  41400  lzenom  41494  irrapxlem2  41547  irrapxlem3  41548  irrapxlem5  41550  pellexlem2  41554  pell14qrgt0  41583  pellfundlb  41608  pellfundex  41610  pellfund14  41622  rmspecsqrtnq  41630  jm2.24nn  41684  jm2.17a  41685  jm2.17b  41686  congabseq  41699  acongrep  41705  acongeq  41708  jm2.26lem3  41726  jm2.27a  41730  jm2.27c  41732  hbtlem2  41852  dgraaub  41876  idomodle  41924  safesnsupfidom1o  42154  sqrtcval  42378  relexpxpmin  42454  frege102d  42491  hashnzfzclim  43067  binomcxplemfrat  43096  binomcxplemnotnn0  43101  suprnmpt  43856  mpct  43886  rnmptbddlem  43934  dstregt0  43978  lefldiveq  43989  fzisoeu  43997  upbdrech  44002  ssfiunibd  44006  fzdifsuc2  44007  xadd0ge  44017  supxrgere  44030  supxrge  44035  suplesup  44036  xrlexaddrp  44049  infxrunb2  44065  infleinflem2  44068  reclt0d  44084  infrpgernmpt  44162  rexanuz2nf  44190  ioondisj2  44193  iccshift  44218  iooshift  44222  fmul01  44283  fmul01lt1lem1  44287  fmul01lt1lem2  44288  climrec  44306  climsuse  44311  mullimc  44319  mullimcf  44326  constlimc  44327  idlimc  44329  divcnvg  44330  limcperiod  44331  limcrecl  44332  lptioo2  44334  lptioo1  44335  islpcn  44342  lptre2pt  44343  limcleqr  44347  neglimc  44350  addlimc  44351  0ellimcdiv  44352  limclner  44354  climleltrp  44379  limsuplesup  44402  limsupmnflem  44423  supcnvlimsupmpt  44444  0cnv  44445  xlimconst  44528  xlimliminflimsup  44565  sinaover2ne0  44571  cncfshift  44577  cncfperiod  44582  cncfioobdlem  44599  cncfioobd  44600  fperdvper  44622  dvdivbd  44626  dvbdfbdioolem1  44631  dvbdfbdioolem2  44632  ioodvbdlimc1lem1  44634  ioodvbdlimc1lem2  44635  ioodvbdlimc2lem  44637  dvnmul  44646  dvnprodlem1  44649  itgiccshift  44683  itgperiod  44684  ismbl3  44689  ovolsplit  44691  stoweidlem1  44704  stoweidlem11  44714  stoweidlem13  44716  stoweidlem14  44717  stoweidlem16  44719  stoweidlem21  44724  stoweidlem25  44728  stoweidlem26  44729  stoweidlem36  44739  stoweidlem38  44741  stoweidlem41  44744  stoweidlem42  44745  stoweidlem45  44748  stoweidlem48  44751  stoweidlem52  44755  stoweidlem62  44765  wallispilem3  44770  stirlinglem5  44781  stirlinglem6  44782  stirlinglem7  44783  stirlinglem10  44786  stirlinglem12  44788  stirlinglem15  44791  dirkercncflem1  44806  fourierdlem10  44820  fourierdlem12  44822  fourierdlem15  44825  fourierdlem16  44826  fourierdlem19  44829  fourierdlem20  44830  fourierdlem21  44831  fourierdlem22  44832  fourierdlem24  44834  fourierdlem30  44840  fourierdlem37  44847  fourierdlem39  44849  fourierdlem40  44850  fourierdlem41  44851  fourierdlem42  44852  fourierdlem47  44856  fourierdlem48  44857  fourierdlem49  44858  fourierdlem50  44859  fourierdlem52  44861  fourierdlem54  44863  fourierdlem60  44869  fourierdlem61  44870  fourierdlem63  44872  fourierdlem64  44873  fourierdlem68  44877  fourierdlem71  44880  fourierdlem72  44881  fourierdlem73  44882  fourierdlem74  44883  fourierdlem75  44884  fourierdlem76  44885  fourierdlem77  44886  fourierdlem78  44887  fourierdlem79  44888  fourierdlem81  44890  fourierdlem82  44891  fourierdlem83  44892  fourierdlem84  44893  fourierdlem87  44896  fourierdlem92  44901  fourierdlem93  44902  fourierdlem94  44903  fourierdlem101  44910  fourierdlem102  44911  fourierdlem103  44912  fourierdlem104  44913  fourierdlem111  44920  fourierdlem112  44921  fourierdlem113  44922  fourierdlem114  44923  sqwvfoura  44931  sqwvfourb  44932  fouriersw  44934  elaa2lem  44936  etransclem23  44960  etransclem28  44965  etransclem32  44969  etransclem35  44972  etransclem48  44985  qndenserrnbllem  44997  rrnprjdstle  45004  ioorrnopnlem  45007  ioorrnopnxrlem  45009  salexct  45037  sge0fsum  45090  sge0supre  45092  sge0rnbnd  45096  sge0lefi  45101  sge0lessmpt  45102  sge0ltfirp  45103  sge0prle  45104  sge0resrnlem  45106  sge0le  45110  sge0split  45112  sge0iunmptlemre  45118  sge0iunmpt  45121  sge0isum  45130  sge0xaddlem1  45136  sge0xaddlem2  45137  sge0xadd  45138  sge0reuz  45150  sge0reuzb  45151  meaunle  45167  meaiunlelem  45171  voliunsge0lem  45175  meaiuninc  45184  meaiininclem  45189  omeunle  45219  omeiunle  45220  omelesplit  45221  omeiunltfirp  45222  carageniuncllem2  45225  caratheodorylem2  45230  caragencmpl  45238  ovnlecvr  45261  ovncvrrp  45267  ovnsubaddlem1  45273  ovnsubadd  45275  hoidmv1lelem1  45294  hoidmv1lelem2  45295  hoidmv1le  45297  hoidmvlelem1  45298  hoidmvlelem2  45299  hoidmvlelem5  45302  hoidmvle  45303  ovnhoilem1  45304  ovnlecvr2  45313  ovncvr2  45314  hoiqssbllem2  45326  hspmbllem2  45330  hspmbllem3  45331  ovnsplit  45351  ovolval5lem1  45355  vonioolem1  45383  vonioolem2  45384  vonicclem1  45386  vonicclem2  45387  pimconstlt1  45405  smflimlem2  45475  smflimlem4  45477  smfmullem1  45494  smfsuplem1  45514  smflimsuplem4  45526  smflimsuplem5  45527  upwordnul  45581  iccpartltu  46080  iccpartleu  46083  pgrple2abl  46995  difmodm1lt  47162  nnpw2blen  47220  dignn0flhalflem1  47255  2itscp  47421