Theorem eqbrtrd 4990

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

Syntax hints:   → wi 4   = wceq 1525   class class class wbr 4968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-rab 3116  df-v 3442  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-sn 4479  df-pr 4481  df-op 4485  df-br 4969

This theorem is referenced by:  eqbrtrrd  4992  somin2  5878  en1b  8432  domunsncan  8471  fodomfi  8650  infsupprpr  8821  hartogslem1  8859  wemaplem2  8864  infdifsn  8973  carddomi2  9252  djuinf  9467  carden  9826  alephsuc3  9855  fpwwe2lem6  9910  fpwwe2lem7  9911  inar1  10050  rankcf  10052  lesub3d  11112  lbinfle  11450  supadd  11463  supmul  11467  rpnnen1lem3  12232  divge1  12311  xrmin1  12424  xrmin2  12425  ifle  12444  qbtwnxr  12447  xltnegi  12463  xleadd1a  12500  xlt2add  12507  xlemul1a  12535  xov1plusxeqvd  12738  ubmelm1fzo  12987  flflp1  13031  ceim1l  13069  ceilm1lt  13070  ceille  13072  quoremz  13077  quoremnn0ALT  13079  modlt  13102  modeqmodmin  13163  addmodlteq  13168  seqf1olem1  13263  bernneq  13444  discr  13455  faclbnd2  13505  faclbnd4lem3  13509  hashun2  13596  hashfun  13650  ccatsymb  13784  ccatrn  13791  sqrlem6  14445  sqrlem7  14446  rddif  14538  amgm2  14567  icodiamlt  14633  climconst  14738  rlimconst  14739  serclim0  14772  rlimcn1  14783  mulcn2  14790  reccn2  14791  o1mul  14809  o1rlimmul  14813  iserex  14851  climlec2  14853  iserge0  14855  climcau  14865  caucvgrlem  14867  caucvgr  14870  iseraltlem2  14877  iseraltlem3  14878  iseralt  14879  fsumabs  14993  o1fsum  15005  iserabs  15007  climfsum  15012  isumless  15037  climcndslem2  15042  divrcnv  15044  flo1  15046  supcvg  15048  georeclim  15065  geomulcvg  15069  cvgrat  15076  mertenslem1  15077  prodfclim1  15086  fprodle  15187  efcvgfsum  15276  eftlub  15299  eflegeo  15311  tanhlt1  15350  tanhbnd  15351  ef01bndlem  15374  sin01bnd  15375  cos01bnd  15376  cos01gt0  15381  ruclem2  15422  ruclem3  15423  ruclem9  15428  ruclem11  15430  ruclem12  15431  bitsfzolem  15620  bitsfzo  15621  bitsinv1lem  15627  sadcaddlem  15643  mulgcd  15729  eucalglt  15762  lcmledvds  15776  lcmfledvds  15809  mulgcddvds  15832  coprmproddvdslem  15839  prmind2  15862  isprm5  15884  divdenle  15922  nonsq  15932  pythagtriplem4  15989  pclem  16008  pcpremul  16013  pczdvds  16032  pcprmpw2  16051  qexpz  16070  prmreclem4  16088  prmreclem5  16089  4sqlem10  16116  ramtub  16181  ramub2  16183  prmodvdslcmf  16216  prmgaplem8  16227  natpropd  17079  catciso  17200  p0le  17486  acsdomd  17624  qusgrp  18092  f1otrspeq  18310  pmtrfrn  18321  pmtrfconj  18329  symggen  18333  psgnunilem4  18360  oddvds2  18427  odcau  18463  pgpfi  18464  pgpssslw  18473  sylow3lem4  18489  efgred2  18610  frgp0  18617  odadd2  18696  oddvdssubg  18702  ablfac1c  18914  ablfac1eu  18916  pgpfaclem3  18926  isabvd  19285  abvsubtri  19300  mplsubrg  19912  coe1sfi  20068  cyggic  20405  mp2pm2mplem5  21106  en2top  21281  1stcrest  21749  2ndcrest  21750  hausmapdom  21796  ufilen  22226  xmetrtri2  22653  prdsxmetlem  22665  bl2in  22697  xblcntrps  22707  xblcntr  22708  ssblps  22719  ssbl  22720  blssps  22721  blss  22722  blcld  22802  methaus  22817  metustexhalf  22853  nmtri2  22923  tngngp3  22952  nrginvrcnlem  22987  nrginvrcn  22988  nmoi  23024  nmo0  23031  nmoid  23038  blcvx  23093  reperflem  23113  reconnlem2  23122  metdcnlem  23131  metdscn  23151  metnrmlem3  23156  mulc1cncf  23200  iccpnfhmeo  23236  cnheiborlem  23245  cnheibor  23246  lebnumii  23257  pcopt  23313  pcopt2  23314  pcoass  23315  nmoleub2lem  23405  nmoleub2lem3  23406  nmoleub2lem2  23407  ipcau2  23524  tcphcphlem1  23525  nglmle  23592  trirn  23690  rrxdstprj1  23699  minveclem3  23719  ivthlem2  23740  ivthlem3  23741  ivth2  23743  ovollb  23767  ovolsslem  23772  ovollb2lem  23776  ovolctb  23778  ovoliunlem1  23790  ovolsca  23803  ovolicc1  23804  ovolicc2lem4  23808  nulmbl  23823  ioombl1lem4  23849  uniioovol  23867  uniioombllem3a  23872  uniioombllem4  23874  opnmbllem  23889  volcn  23894  volivth  23895  i1fadd  23983  i1fmul  23984  mbfi1fseqlem4  24006  mbfi1fseqlem5  24007  mbfi1fseqlem6  24008  itg2const2  24029  itg2seq  24030  itg2uba  24031  itg2split  24037  itg2monolem1  24038  itg2monolem3  24040  itg2i1fseq2  24044  itg2addlem  24046  itg2gt0  24048  itg2cnlem1  24049  itg2cnlem2  24050  itgless  24104  ibladdlem  24107  bddmulibl  24126  dveflem  24263  dvferm1lem  24268  dvferm2lem  24270  dvlip  24277  dvlipcn  24278  dvlip2  24279  dvle  24291  dvivthlem1  24292  lhop1lem  24297  dvcvx  24304  dvfsumabs  24307  dvfsumlem2  24311  dvfsumlem4  24313  dvfsumrlim2  24316  dvfsum2  24318  ftc1a  24321  ftc1lem4  24323  ftc1lem5  24324  deg1sub  24389  ply1divex  24417  deg1submon1p  24433  r1pdeglt  24439  dvdsq1p  24441  fta1glem2  24447  fta1g  24448  plyeq0lem  24487  dgrlt  24543  fta1lem  24583  aalioulem2  24609  aalioulem3  24610  aalioulem4  24611  aaliou3lem2  24619  aaliou3lem9  24626  taylply2  24643  ulmbdd  24673  ulmdvlem1  24675  mtest  24679  mtestbdd  24680  radcnvlem1  24688  radcnvle  24695  pserulm  24697  psercn  24701  pserdvlem2  24703  abelthlem2  24707  abelthlem5  24710  abelthlem7  24713  abelthlem8  24714  abelthlem9  24715  reeff1olem  24721  tangtx  24778  tanord  24807  efif1olem4  24814  logrnaddcl  24843  logcj  24874  logimul  24882  logneg2  24883  logdivlti  24888  divlogrlim  24903  logcnlem3  24912  logcnlem4  24913  efopn  24926  logtayllem  24927  logtayl  24928  cxpcn3lem  25013  cxpaddle  25018  abscxpbnd  25019  asinlem3  25134  asinneg  25149  asinsin  25155  atanlogaddlem  25176  atantan  25186  bndatandm  25192  atans2  25194  atantayl  25200  atantayl2  25201  atantayl3  25202  leibpi  25206  birthdaylem3  25217  rlimcnp  25229  efrlim  25233  cxplim  25235  cxp2lim  25240  cxploglim2  25242  divsqrtsumo1  25247  jensenlem2  25251  amgm  25254  logdifbnd  25257  harmonicbnd4  25274  fsumharmonic  25275  lgamgulmlem2  25293  lgamgulmlem3  25294  lgamgulmlem5  25296  lgambdd  25300  lgamcvg2  25318  ftalem1  25336  ftalem5  25340  basellem1  25344  basellem8  25351  ppip1le  25424  ppiltx  25440  sqff1o  25445  chtublem  25473  chpub  25482  logfaclbnd  25484  logfacrlim  25486  logexprlim  25487  mersenne  25489  bcmono  25539  bcmax  25540  bposlem2  25547  bposlem5  25550  lgslem3  25561  gausslemma2dlem1a  25627  lgsquadlem1  25642  lgsquadlem2  25643  2lgslem1c  25655  2sqblem  25693  chebbnd1  25734  chtppilimlem1  25735  chto1ub  25738  chpchtlim  25741  chpo1ubb  25743  rplogsumlem1  25746  rplogsumlem2  25747  rpvmasumlem  25749  dchrisumlem1  25751  dchrisumlem2  25752  dchrmusum2  25756  dchrvmasumlem2  25760  dchrvmasumlem3  25761  dchrvmasumiflem1  25763  dchrisum0flblem1  25770  dchrisum0fno1  25773  dchrisum0lem1b  25777  dchrisum0lem1  25778  dchrisum0lem2a  25779  dchrisum0lem2  25780  rplogsum  25789  mudivsum  25792  mulogsumlem  25793  mulog2sumlem1  25796  mulog2sumlem2  25797  vmalogdivsum2  25800  2vmadivsumlem  25802  selberglem2  25808  selberg2b  25814  logdivbnd  25818  selberg3lem1  25819  selberg3lem2  25820  selberg4lem1  25822  pntrmax  25826  pntrsumo1  25827  pntrlog2bndlem1  25839  pntrlog2bndlem2  25840  pntrlog2bndlem3  25841  pntrlog2bndlem4  25842  pntrlog2bndlem5  25843  pntrlog2bnd  25846  pntpbnd1a  25847  pntpbnd2  25849  pntibndlem2  25853  pntlemb  25859  pntlemg  25860  pntlemh  25861  pntlemr  25864  pntlemj  25865  pntlemf  25867  pntlemo  25869  pnt  25876  padicabv  25892  ostth2lem2  25896  ostth2lem3  25897  ostth3  25900  colperpexlem3  26204  mideulem2  26206  lnperpex  26275  trgcopy  26276  iscgra1  26282  brbtwn2  26378  colinearalglem4  26382  subupgr  26756  crctcshwlkn0lem1  27274  nvabs  28136  nvge0  28137  smcnlem  28161  nmblolbii  28263  blocnilem  28268  siii  28317  ubthlem2  28335  minvecolem3  28340  htthlem  28381  bcsiALT  28643  bcs3  28647  chscllem4  29104  0cnop  29443  0cnfn  29444  nmbdoplbi  29488  nmcoplbi  29492  nmophmi  29495  nmbdfnlbi  29513  nmcfnlbi  29516  nlelchi  29525  riesz1  29529  cnlnadjlem2  29532  nmopadjlei  29552  nmoptrii  29558  nmopcoi  29559  nmopcoadji  29565  unierri  29568  branmfn  29569  pjs14i  29674  hstle  29694  cdj3lem2b  29901  xlt2addrd  30166  eliccelico  30184  elicoelioo  30185  ltesubnnd  30218  pfxlsw2ccat  30301  wrdt2ind  30302  archirngz  30452  archiabllem2c  30458  madjusmdetlem2  30704  locfinref  30718  sqsscirc1  30764  tpr2rico  30768  esumcst  30935  esumgect  30962  esum2d  30965  measunl  31088  measiun  31090  omssubaddlem  31170  omssubadd  31171  carsgsigalem  31186  carsgclctunlem2  31190  pmeasmono  31195  eulerpartlemgc  31233  eulerpartlemb  31239  ballotlemsel1i  31383  ballotlemro  31393  sgnsub  31415  signsplypnf  31433  signsply0  31434  signsvtn  31467  signsvfnn  31469  hgt750lemd  31532  logdivsqrle  31534  hashf1dmcdm  31966  erdsze2lem1  32060  sinccvglem  32525  divcnvlin  32574  iprodefisum  32583  faclimlem2  32586  nosep1o  32797  nodense  32807  fnemeet1  33325  dnibndlem10  33437  dnibndlem11  33438  dnibnd  33441  knoppcnlem4  33446  knoppcnlem6  33448  unblimceq0lem  33456  unbdqndv2lem1  33459  unbdqndv2lem2  33460  knoppndvlem11  33472  knoppndvlem12  33473  knoppndvlem14  33475  knoppndvlem15  33476  knoppndvlem17  33478  knoppndvlem18  33479  knoppndvlem19  33480  knoppndvlem21  33482  ctbssinf  34239  ltflcei  34432  ptrecube  34444  poimirlem16  34460  poimirlem17  34461  poimirlem29  34473  broucube  34478  opnmbllem0  34480  mblfinlem2  34482  mblfinlem3  34483  ismblfin  34485  itg2addnclem  34495  itg2addnclem2  34496  itg2addnclem3  34497  itg2addnc  34498  ibladdnclem  34500  ftc1cnnclem  34517  ftc1cnnc  34518  ftc1anc  34527  geomcau  34587  prdsbnd  34624  cntotbnd  34627  heiborlem4  34645  rrndstprj2  34662  rrncmslem  34663  rrnequiv  34666  iccbnd  34671  cvlcvr1  36027  cvrat3  36130  dalem25  36386  cdlema1N  36479  dalawlem3  36561  dalawlem4  36562  dalawlem5  36563  dalawlem6  36564  dalawlem7  36565  dalawlem9  36567  dalawlem11  36569  dalawlem12  36570  lhp2lt  36689  lhpmcvr  36711  4atexlemcnd  36760  lautj  36781  trlle  36872  trlval3  36875  trlval4  36876  cdleme0moN  36913  cdleme13  36960  cdleme15  36966  cdleme19b  36992  cdleme20e  37001  cdleme20j  37006  cdleme22e  37032  cdleme22eALTN  37033  cdleme26fALTN  37050  cdleme26f  37051  cdleme27N  37057  cdleme41sn3a  37121  cdleme46fsvlpq  37193  cdlemeg46vrg  37215  cdlemg4  37305  cdlemg7N  37314  cdlemg9a  37320  cdlemg11b  37330  cdlemg12a  37331  trljco  37428  tendoidcl  37457  tendococl  37460  tendopltp  37468  tendo0tp  37477  tendoicl  37484  cdlemi2  37507  cdlemk5a  37523  cdlemk5  37524  cdlemk12  37538  cdlemkole  37541  cdlemk14  37542  cdlemk12u  37560  cdlemk37  37602  cdlemk39s-id  37628  cdlemk49  37639  cdlemk39u1  37655  cdlemk39u  37656  dian0  37727  cdlemm10N  37806  cdlemn2  37883  cdlemn10  37894  dihord1  37906  dihord10  37911  dihmeetlem4preN  37994  dihmeetlem18N  38012  dihmeetlem20N  38014  dihjatc  38105  mapdcnvatN  38354  fltltc  38791  lzenom  38873  irrapxlem2  38926  irrapxlem3  38927  irrapxlem5  38929  pellexlem2  38933  pell14qrgt0  38962  pellfundlb  38987  pellfundex  38989  pellfund14  39001  rmspecsqrtnq  39009  jm2.24nn  39062  jm2.17a  39063  jm2.17b  39064  congabseq  39077  acongrep  39083  acongeq  39086  jm2.26lem3  39104  jm2.27a  39108  jm2.27c  39110  hbtlem2  39230  dgraaub  39254  idomodle  39302  relexpxpmin  39568  frege102d  39605  triv1nsgd  40159  2nsgsimpgd  40179  hashnzfzclim  40213  binomcxplemfrat  40242  binomcxplemnotnn0  40247  suprnmpt  40991  mpct  41025  rnmptbddlem  41077  dstregt0  41109  lefldiveq  41121  fzisoeu  41129  upbdrech  41134  ssfiunibd  41138  fzdifsuc2  41139  xadd0ge  41150  supxrgere  41163  supxrge  41168  suplesup  41169  xrlexaddrp  41182  infxrunb2  41198  infleinflem2  41201  reclt0d  41220  infrpgernmpt  41304  ioondisj2  41330  iccshift  41357  iooshift  41361  fmul01  41424  fmul01lt1lem1  41428  fmul01lt1lem2  41429  climrec  41447  climsuse  41452  mullimc  41460  mullimcf  41467  constlimc  41468  idlimc  41470  divcnvg  41471  limcperiod  41472  limcrecl  41473  lptioo2  41475  lptioo1  41476  islpcn  41483  lptre2pt  41484  limcleqr  41488  neglimc  41491  addlimc  41492  0ellimcdiv  41493  limclner  41495  climleltrp  41520  limsuplesup  41543  limsupmnflem  41564  supcnvlimsupmpt  41585  0cnv  41586  xlimconst  41669  xlimliminflimsup  41706  sinaover2ne0  41712  cncfshift  41720  cncfperiod  41725  cncfioobdlem  41742  cncfioobd  41743  fperdvper  41766  dvdivbd  41771  dvbdfbdioolem1  41776  dvbdfbdioolem2  41777  ioodvbdlimc1lem1  41779  ioodvbdlimc1lem2  41780  ioodvbdlimc2lem  41782  dvnmul  41791  dvnprodlem1  41794  itgiccshift  41828  itgperiod  41829  ismbl3  41835  ovolsplit  41837  stoweidlem1  41850  stoweidlem11  41860  stoweidlem13  41862  stoweidlem14  41863  stoweidlem16  41865  stoweidlem21  41870  stoweidlem25  41874  stoweidlem26  41875  stoweidlem36  41885  stoweidlem38  41887  stoweidlem41  41890  stoweidlem42  41891  stoweidlem45  41894  stoweidlem48  41897  stoweidlem52  41901  stoweidlem62  41911  wallispilem3  41916  stirlinglem5  41927  stirlinglem6  41928  stirlinglem7  41929  stirlinglem10  41932  stirlinglem12  41934  stirlinglem15  41937  dirkercncflem1  41952  fourierdlem10  41966  fourierdlem12  41968  fourierdlem15  41971  fourierdlem16  41972  fourierdlem19  41975  fourierdlem20  41976  fourierdlem21  41977  fourierdlem22  41978  fourierdlem24  41980  fourierdlem30  41986  fourierdlem37  41993  fourierdlem39  41995  fourierdlem40  41996  fourierdlem41  41997  fourierdlem42  41998  fourierdlem47  42002  fourierdlem48  42003  fourierdlem49  42004  fourierdlem50  42005  fourierdlem52  42007  fourierdlem54  42009  fourierdlem60  42015  fourierdlem61  42016  fourierdlem63  42018  fourierdlem64  42019  fourierdlem68  42023  fourierdlem71  42026  fourierdlem72  42027  fourierdlem73  42028  fourierdlem74  42029  fourierdlem75  42030  fourierdlem76  42031  fourierdlem77  42032  fourierdlem78  42033  fourierdlem79  42034  fourierdlem81  42036  fourierdlem82  42037  fourierdlem83  42038  fourierdlem84  42039  fourierdlem87  42042  fourierdlem92  42047  fourierdlem93  42048  fourierdlem94  42049  fourierdlem101  42056  fourierdlem102  42057  fourierdlem103  42058  fourierdlem104  42059  fourierdlem111  42066  fourierdlem112  42067  fourierdlem113  42068  fourierdlem114  42069  sqwvfoura  42077  sqwvfourb  42078  fouriersw  42080  elaa2lem  42082  etransclem23  42106  etransclem28  42111  etransclem32  42115  etransclem35  42118  etransclem48  42131  qndenserrnbllem  42143  rrnprjdstle  42150  ioorrnopnlem  42153  ioorrnopnxrlem  42155  salexct  42181  sge0fsum  42233  sge0supre  42235  sge0rnbnd  42239  sge0lefi  42244  sge0lessmpt  42245  sge0ltfirp  42246  sge0prle  42247  sge0resrnlem  42249  sge0le  42253  sge0split  42255  sge0iunmptlemre  42261  sge0iunmpt  42264  sge0isum  42273  sge0xaddlem1  42279  sge0xaddlem2  42280  sge0xadd  42281  sge0reuz  42293  sge0reuzb  42294  meaunle  42310  meaiunlelem  42314  voliunsge0lem  42318  meaiuninc  42327  meaiininclem  42332  omeunle  42362  omeiunle  42363  omelesplit  42364  omeiunltfirp  42365  carageniuncllem2  42368  caratheodorylem2  42373  caragencmpl  42381  ovnlecvr  42404  ovncvrrp  42410  ovnsubaddlem1  42416  ovnsubadd  42418  hoidmv1lelem1  42437  hoidmv1lelem2  42438  hoidmv1le  42440  hoidmvlelem1  42441  hoidmvlelem2  42442  hoidmvlelem5  42445  hoidmvle  42446  ovnhoilem1  42447  ovnlecvr2  42456  ovncvr2  42457  hoiqssbllem2  42469  hspmbllem2  42473  hspmbllem3  42474  ovnsplit  42494  ovolval5lem1  42498  vonioolem1  42526  vonioolem2  42527  vonicclem1  42529  vonicclem2  42530  pimconstlt1  42547  smflimlem2  42612  smflimlem4  42614  smfmullem1  42630  smfsuplem1  42649  smflimsuplem4  42661  smflimsuplem5  42662  iccpartltu  43089  iccpartleu  43092  pgrple2abl  43915  difmodm1lt  44085  nnpw2blen  44143  dignn0flhalflem1  44178  2itscp  44271