Theorem eleqtrrdi 2871

Description: A membership and equality inference. (Contributed by NM, 24-Apr-2005.)

Hypotheses

Ref	Expression
eleqtrrdi.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)
eleqtrrdi.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
eleqtrrdi	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eleqtrrdi

Step	Hyp	Ref	Expression
1		eleqtrrdi.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		eleqtrrdi.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2769	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eleqtrdi 2870	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-clel 2835

This theorem is used by:  3eltr4g  2877  srcmpltd  4432  brelrng  5925  elabrex  7240  elabrexg  7241  fliftel1  7312  ovidig  7556  unielxp  8025  tfrlem11  8378  rdglim  8416  seqomlem4  8445  2oconcl  8493  ecopqsi  8773  erov  8817  eroprf  8818  sbthlem2  9089  dffi3  9404  ixpiunwdom  9565  cantnfcl  9649  r1lim  9757  rankwflemb  9778  pwwf  9792  unwf  9795  rankwflem  9800  uniwf  9804  rankpwi  9808  rankr1g  9817  r1pw  9830  r1rankid  9844  rankuni  9848  djulcl  9918  djurcl  9919  inlresf  9922  inrresf  9924  djuun  9934  cardlim  9980  infxpenlem  10019  alephfp  10114  cfsmolem  10275  alephsing  10281  hsmexlem4  10434  axdc3lem2  10456  numth3  10475  iunfo  10550  konigthlem  10580  iunctb  10586  canthwelem  10662  canthwe  10663  r1limwun  10748  inar1  10787  inatsk  10790  gruina  10830  grur1  10832  tskmval  10851  tskmcl  10853  pinq  10939  dmrecnq  10980  addclsr  11095  mulclsr  11096  axaddf  11157  axmulf  11158  peano2nn  12272  uztrn2  12909  eluz2nn  12940  peano2uzs  12954  uzsupss  12992  uzsup  13927  uzrdgfni  14025  uzrdgsuci  14027  fsuppmapnn0fiub  14058  seqf  14090  ser0  14121  bcm1k  14382  bcp1nk  14384  bcpasc  14388  hashprdifel  14465  fz1isolem  14529  pr2pwpr  14547  tpf  14567  ccats1val2  14698  rexuzre  15443  limsupgre  15571  climconst  15633  rlimclim1  15635  climrlim2  15637  clim2ser  15745  clim2ser2  15746  iserex  15747  isermulc2  15748  iserle  15750  isercolllem3  15757  isercoll2  15759  climsup  15760  iseraltlem2  15773  iseraltlem3  15774  zsum  15807  isumclim3  15848  isumadd  15856  fsump1i  15858  iserabs  15905  cvgcmp  15906  cvgcmpub  15907  cvgcmpce  15908  abscvgcvg  15909  isumshft  15931  isumsplit  15932  isum1p  15933  isumrpcl  15935  isumsup2  15938  climcndslem1  15941  cvgrat  15975  clim2prod  15980  clim2div  15981  prodf1  15983  ntrivcvgn0  15990  ntrivcvgtail  15992  fprodntriv  16032  fprodabs  16064  fprodeq0  16065  iprodclim3  16090  iprodmul  16093  ef0lem  16167  fprodefsum  16184  rpnnen2lem3  16307  dvdsflip  16410  fzo0dvdseq  16416  bitsinv1  16535  smupval  16581  smueqlem  16583  seq1st  16664  algr0  16665  prmind2  16778  crth  16872  eulerthlem2  16876  prmdiv  16879  pockthlem  17000  pockthg  17001  unbenlem  17003  prmunb  17009  prmgaplem7  17152  strfv2d  17296  imasvscaval  17627  oppccatid  17810  oppccatf  17819  epii  17835  fthepi  18022  funcestrcsetclem3  18233  funcsetcestrclem3  18247  yon12  18356  yon2  18357  yonedalem4c  18368  yonedalem22  18369  yonedalem3b  18370  yonedainv  18372  acsmapd  18645  chnub  18713  chnccats1  18716  chnccat  18717  mgm2nsgrplem1  19033  mgm2nsgrplem2  19034  mgm2nsgrplem3  19035  sgrp2nmndlem1  19038  sgrp2rid2  19041  ghmqusker  19417  cntrsubgnsg  19473  symgpssefmnd  19526  pmtrrn  19587  gexcl3  19717  efgi  19849  efgi2  19855  efgs1b  19866  efgredlemg  19872  efgredlemd  19874  frgpnabllem1  20003  cycsubgcyg  20031  gsumzaddlem  20051  dprdwd  20143  dprd2da  20174  rhmopp  20672  lsppratlem3  21339  lsppratlem4  21340  lbsextlem2  21349  lidl0ALT  21420  lidl1ALT  21423  2idl0  21465  2idl1  21466  rhmpreimaprmidl  21545  ssdifidllem  21550  ssdifidl  21551  domnchr  21748  znf1o  21767  mplsubrglem  22221  mpfconst  22328  mpfproj  22329  mpfind  22334  mhpmulcl  22380  pf1const  22574  pf1id  22575  mpfpf1  22579  pf1mpf  22580  madetsumid  22686  slesolex  22910  pmatcoe1fsupp  22929  mat2pmatbas0  22955  pmatcollpw  23009  pm2mpf1  23027  isclo  23315  indiscld  23319  restntr  23410  ordtbaslem  23416  ordtbas2  23419  lmconst  23489  lmss  23526  conncompid  23659  2ndcomap  23687  locfincmp  23755  comppfsc  23761  xkouni  23828  txcls  23833  ptclsg  23844  uptx  23854  txindis  23863  tx1stc  23879  cnmpt1res  23905  tgqtop  23941  uffix  24150  cnpflf2  24229  ptcmplem2  24282  ptcmplem4  24284  tgpconncomp  24342  tsmsfbas  24357  fmucnd  24520  prdsxmetlem  24597  imasdsf1olem  24602  prdsbl  24720  blcvx  25027  xrsmopn  25042  xrge0tsms  25064  metdcn2  25069  expcncf  25157  cnmpopc  25159  icchmeo  25172  iccpnfhmeo  25176  cnheibor  25186  evth  25190  evth2  25191  lebnumlem2  25193  lebnumii  25197  reparphti  25228  cfilfcls  25505  minveclem2  25657  minveclem3  25660  minveclem4  25663  ovoliunlem1  25733  ovolicc1  25747  iundisj  25779  volsup  25787  uniioombllem3  25816  vitalilem2  25840  vitalilem3  25841  mbfsup  25895  mbfinf  25896  mbflimsup  25897  itg2monolem1  25981  limcflflem  26110  limccnp  26121  limccnp2  26122  dvidlem  26145  dvn2bss  26160  cpnres  26167  dvcobr  26176  dvrec  26185  c1liplem1  26226  dvcnvrelem2  26248  dvfsumrlimf  26255  dvfsumlem1  26256  dvfsumlem2  26257  dvfsumlem3  26258  dvfsumlem4  26259  dvfsumrlim  26261  dvfsum2  26264  coeeulem  26453  coeid3  26469  plycn  26490  dvntaylp  26610  taylthlem1  26612  taylthlem2  26613  ulm2  26624  ulmshftlem  26628  ulmshft  26629  ulm0  26630  ulmcn  26638  ulmdvlem3  26641  ulmdv  26642  mtest  26643  mtestbdd  26644  dvradcnv  26660  psercn2  26662  psercn  26665  pserdv  26668  abelth  26680  efif1olem2  26783  efif1olem4  26785  efifo  26787  eff1olem  26788  logcn  26887  dvloglem  26888  cxpcn3  26988  resqrtcn  26989  sqrtcn  26990  logbleb  27023  logblt  27024  asinneg  27126  atanlogsub  27156  atanbnd  27166  ressatans  27174  leibpilem2  27181  xrlimcnp  27208  efrlim  27209  scvxcvx  27225  ppiub  27443  chtub  27451  logexprlim  27464  lgseisenlem1  27614  rplogsumlem1  27723  rplogsumlem2  27724  dchrisumlem2  27729  dchrisum0flb  27749  logdivbnd  27795  pntlem3  27848  dfnns2  28640  tgcgr4  28876  ltgov  28942  elcgrabasrd  29258  cgrabasimass  29260  f1otrg  29330  eengtrkg  29446  iedgedg  29510  ushgredgedgloop  29694  subgruhgredgd  29747  uvtxupgrres  29871  umgr2v2evd2  29990  edginwlk  30097  wlk1walk  30101  crctcshwlkn0lem6  30286  wlkiswwlks1  30338  minvecolem1  31358  minvecolem2  31359  minvecolem4  31364  htthlem  31401  5oalem2  32139  3oalem2  32147  iundisjf  33065  fmptco1f1o  33109  xppreima  33121  xppreima2  33127  dfcnv2  33151  ccatws1f1o  33396  gsumhashmul  33510  xrge0tsmsd  33516  gsumwrd2dccatlem  33520  odpmco  33529  pmtrcnelor  33534  fzo0pmtrlast  33535  wrdpmtrlast  33536  pmtrto1cl  33542  psgnfzto1stlem  33543  fzto1stfv1  33544  fzto1st  33546  fzto1stinvn  33547  psgnfzto1st  33548  tocycf  33560  cycpmco2lem7  33575  cycpmco2  33576  cycpmrn  33586  cyc3evpm  33593  cyc3genpmlem  33594  cycpmgcl  33596  cyc3conja  33600  elrgspnlem1  33685  elrgspnlem2  33686  elrgspnlem3  33687  elrgspnlem4  33688  elrgspnsubrunlem1  33690  nsgmgc  33844  nsgqusf1olem1  33845  nsgqusf1olem2  33846  ssmxidllem  33879  drngmxidlr  33883  opprqus1r  33897  qsdrngilem  33899  qsdrngi  33900  rsprprmprmidlb  33936  rprmirredb  33945  1arithufdlem1  33957  1arithufdlem2  33958  1arithufdlem3  33959  1arithufdlem4  33960  fply1  33971  ply1degltel  34007  ply1degleel  34008  ply1degltlss  34009  mplmulmvr  34052  psrmon  34062  psrmonprod  34065  esplylem  34079  esplyfv1  34082  esplysply  34084  esplyind  34088  ply1degltdimlem  34135  ply1degltdim  34136  algextdeglem4  34233  algextdeglem6  34235  algextdeglem7  34236  algextdeglem8  34237  nn0constr  34274  smatlem  34310  smatcl  34315  zartopn  34388  zarmxt1  34393  tpr2rico  34425  xrmulc1cn  34443  xrge0mulc1cn  34454  esumpfinvallem  34587  ldgenpisyslem1  34677  dynkin  34681  brfae  34762  sxbrsigalem3  34786  dya2icoseg2  34792  omsmeas  34837  sibfof  34854  sseqmw  34905  sseqf  34906  sseqp1  34909  fiblem  34912  fibp1  34915  probfinmeasbALTV  34943  repr0  35122  reprpmtf1o  35137  hgt750lemg  35165  bnj1379  35342  fineqvnttrclselem3  35652  subfacp1lem5  35766  subfacp1lem6  35767  cvxpconn  35824  cvxsconn  35825  cvmliftlem6  35872  cvmliftlem8  35874  cvmliftlem10  35876  cvmlift2lem6  35890  cvmlift2lem11  35895  cvmlift2lem12  35896  2goelgoanfmla1  36006  prv1n  36013  msubff  36112  msubco  36113  elmsta  36130  msubff1  36138  mvhf  36140  msubvrs  36142  iprodefisumlem  36322  filnetlem3  37002  ttcid  37114  ttcwf  37146  knoppcnlem10  37202  knoppcnlem11  37203  icoreunrn  38116  icoreelrn  38118  ralssiun  38164  poimirlem3  38375  poimirlem16  38388  poimirlem17  38389  poimirlem19  38391  poimirlem30  38402  dvasin  38456  cover2  38468  upixp  38482  sdclem1  38496  fdc  38498  caushft  38514  ismtyres  38561  rrncmslem  38585  isfld2  38758  presuc  39249  osumcllem10N  40841  pexmidlem7N  40852  dihglblem2N  42170  lcfrvalsnN  42417  lcfrlem5  42422  lcfrlem6  42423  lcfrlem27  42445  lcfrlem37  42455  aks6d1c1p4  42980  aks6d1c1p7  42982  aks6d1c1p8  42984  evl1gprodd  42986  aks6d1c2lem4  42996  aks6d1c5lem3  43006  aks6d1c6lem2  43040  prjspvs  43459  0prjspnrel  43476  monotuz  43785  expdiophlem1  43865  kelac2  43909  naddwordnexlem4  44245  grurankcld  45074  dvgrat  45139  nzss  45144  uzmptshftfval  45173  binomcxplemnotnn0  45183  orbitinit  45782  orbitcl  45783  permaxinf2lem  45838  refsumcn  45867  rfcnpre2  45868  rfcnpre3  45870  rfcnpre4  45871  disjf1o  46026  unirnmap  46041  unirnmapsn  46047  ssmapsn  46049  mptssid  46073  allbutfi  46225  eluzd  46240  uzidd2  46247  ressiocsup  46387  ressioosup  46388  ressiooinf  46390  fsumsermpt  46412  climexp  46438  climinf  46439  climsuse  46441  sumnnodd  46463  limsupresico  46531  limsupubuzlem  46543  limsupresxr  46597  liminfresxr  46598  liminfresico  46602  limsup10exlem  46603  cnrefiisplem  46660  cncfiooicclem1  46724  dvsinax  46744  itgsinexplem1  46785  fvvolioof  46820  fvvolicof  46822  stoweidlem14  46845  stoweidlem16  46847  stoweidlem31  46862  stoweidlem34  46865  stoweidlem36  46867  stoweidlem43  46874  stoweidlem46  46877  stoweidlem47  46878  stoweidlem52  46883  stoweidlem55  46886  stoweidlem57  46888  dirkercncf  46938  fourierdlem20  46958  fourierdlem42  46980  fourierdlem51  46988  fourierdlem54  46991  fourierdlem62  46999  fourierdlem71  47008  fourierdlem80  47017  fourierdlem114  47051  fouriersw  47062  ioorrnopnlem  47135  ioorrnopnxrlem  47137  salexct3  47173  salgencntex  47174  salgensscntex  47175  subsalsal  47190  sge0fodjrnlem  47247  sge0isum  47258  sge0seq  47277  sge0reuz  47278  sge0reuzb  47279  meadjiunlem  47296  meaiininclem  47317  carageniuncllem1  47352  caratheodorylem1  47357  hoiprodp1  47419  hoidmv1lelem1  47422  hoidmv1lelem2  47423  hoidmv1le  47425  hoidmvlelem1  47426  hoidmvlelem2  47427  hoidmvlelem3  47428  voncmpl  47452  hoiqssbl  47456  smflimlem2  47603  smfsuplem1  47642  smfsuplem3  47644  fsupdm  47673  finfdm  47677  sinnpoly  47762  cfsetsnfsetf  47949  fcores  47958  afvres  48063  afv2res  48130  fundcmpsurinjimaid  48314  iccpartigtl  48326  sprsymrelf  48398  prproropf1olem2  48407  uhgrimedgi  48809  isuspgrim0lem  48812  isuspgrimlem  48814  ushggricedg  48846  grimedg  48854  usgrgrtrirex  48869  isubgr3stgrlem7  48891  uspgrlimlem4  48910  grlimprclnbgr  48915  gpgiedgdmellem  48965  gpg3kgrtriex  49008  funcringcsetcALTV2lem3  49210  funcringcsetclem3ALTV  49233  lindslinindsimp2lem5  49395  rrxsphere  49681  line2  49685  iooii  49847  icccldii  49848  iscnrm3rlem3  49871  eloppf2  50063  oppcup  50136  natoppf  50158  zeroo2  50163  oppfdiag1  50343  oppfdiag  50345  2arwcat  50529  incat  50530  lmddu  50596  onsetreclem3  50636  amgmwlem  50823