Theorem eleqtrrdi 2843

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 2740	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eleqtrdi 2842	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-clel 2809

This theorem is referenced by:  3eltr4g  2849  brelrng  5901  elabrex  7195  fliftel1  7260  ovidig  7502  unielxp  7964  tfrlem11  8339  rdglim  8377  seqomlem4  8404  2oconcl  8454  ecopqsi  8720  erov  8760  eroprf  8761  sbthlem2  9035  dffi3  9376  ixpiunwdom  9535  cantnfcl  9612  r1lim  9717  rankwflemb  9738  pwwf  9752  unwf  9755  rankwflem  9760  uniwf  9764  rankpwi  9768  rankr1g  9777  r1pw  9790  r1rankid  9804  rankuni  9808  djulcl  9855  djurcl  9856  inlresf  9859  inrresf  9861  djuun  9871  cardlim  9917  infxpenlem  9958  alephfp  10053  cfsmolem  10215  alephsing  10221  hsmexlem4  10374  axdc3lem2  10396  numth3  10415  iunfo  10484  konigthlem  10513  iunctb  10519  canthwelem  10595  canthwe  10596  r1limwun  10681  inar1  10720  inatsk  10723  gruina  10763  grur1  10765  tskmval  10784  tskmcl  10786  pinq  10872  dmrecnq  10913  addclsr  11028  mulclsr  11029  axaddf  11090  axmulf  11091  peano2nn  12174  uztrn2  12791  eluz2nn  12818  peano2uzs  12836  uzsupss  12874  uzsup  13778  uzrdgfni  13873  uzrdgsuci  13875  fsuppmapnn0fiub  13906  seqf  13939  ser0  13970  bcm1k  14225  bcp1nk  14227  bcpasc  14231  hashprdifel  14308  fz1isolem  14372  pr2pwpr  14390  ccats1val2  14527  rexuzre  15249  limsupgre  15375  climconst  15437  rlimclim1  15439  climrlim2  15441  clim2ser  15551  clim2ser2  15552  iserex  15553  isermulc2  15554  iserle  15556  isercolllem3  15563  isercoll2  15565  climsup  15566  iseraltlem2  15579  iseraltlem3  15580  zsum  15614  isumclim3  15655  isumadd  15663  fsump1i  15665  iserabs  15711  cvgcmp  15712  cvgcmpub  15713  cvgcmpce  15714  abscvgcvg  15715  isumshft  15735  isumsplit  15736  isum1p  15737  isumrpcl  15739  isumsup2  15742  climcndslem1  15745  cvgrat  15779  clim2prod  15784  clim2div  15785  prodf1  15787  ntrivcvgn0  15794  ntrivcvgtail  15796  fprodntriv  15836  fprodabs  15868  fprodeq0  15869  iprodclim3  15894  iprodmul  15897  ef0lem  15972  fprodefsum  15988  rpnnen2lem3  16109  dvdsflip  16210  fzo0dvdseq  16216  bitsinv1  16333  smupval  16379  smueqlem  16381  seq1st  16458  algr0  16459  prmind2  16572  crth  16661  eulerthlem2  16665  prmdiv  16668  pockthlem  16788  pockthg  16789  unbenlem  16791  prmunb  16797  prmgaplem7  16940  strfv2d  17085  imasvscaval  17434  oppccatid  17615  oppccatf  17624  epii  17640  fthepi  17829  funcestrcsetclem3  18044  funcsetcestrclem3  18058  yon12  18168  yon2  18169  yonedalem4c  18180  yonedalem22  18181  yonedalem3b  18182  yonedainv  18184  acsmapd  18457  mgm2nsgrplem1  18742  mgm2nsgrplem2  18743  mgm2nsgrplem3  18744  sgrp2nmndlem1  18747  sgrp2rid2  18750  cntrsubgnsg  19135  symgpssefmnd  19191  pmtrrn  19253  gexcl3  19383  efgi  19515  efgi2  19521  efgs1b  19532  efgredlemg  19538  efgredlemd  19540  frgpnabllem1  19665  cycsubgcyg  19692  gsumzaddlem  19712  dprdwd  19804  dprd2da  19835  rhmopp  20198  lsppratlem3  20669  lsppratlem4  20670  lbsextlem2  20679  lidl0  20748  lidl1  20749  domnchr  20972  znf1o  20995  mplsubrglem  21447  mpfconst  21548  mpfproj  21549  mpfind  21554  mhpmulcl  21576  pf1const  21749  pf1id  21750  mpfpf1  21754  pf1mpf  21755  madetsumid  21847  slesolex  22068  pmatcoe1fsupp  22087  mat2pmatbas0  22113  pmatcollpw  22167  pm2mpf1  22185  isclo  22475  indiscld  22479  restntr  22570  ordtbaslem  22576  ordtbas2  22579  lmconst  22649  lmss  22686  conncompid  22819  2ndcomap  22846  locfincmp  22914  comppfsc  22920  xkouni  22987  txcls  22992  ptclsg  23003  uptx  23013  txindis  23022  tx1stc  23038  cnmpt1res  23064  tgqtop  23100  uffix  23309  cnpflf2  23388  ptcmplem2  23441  ptcmplem4  23443  tgpconncomp  23501  tsmsfbas  23516  fmucnd  23681  prdsxmetlem  23758  imasdsf1olem  23763  prdsbl  23884  blcvx  24198  xrsmopn  24212  xrge0tsms  24234  metdcn2  24239  expcncf  24326  cnmpopc  24328  icchmeo  24341  iccpnfhmeo  24345  cnheibor  24355  evth  24359  evth2  24360  lebnumlem2  24362  lebnumii  24366  reparphti  24397  cfilfcls  24675  minveclem2  24827  minveclem3  24830  minveclem4  24833  ovoliunlem1  24903  ovolicc1  24917  iundisj  24949  volsup  24957  uniioombllem3  24986  vitalilem2  25010  vitalilem3  25011  mbfsup  25065  mbfinf  25066  mbflimsup  25067  itg2monolem1  25152  limcflflem  25281  limccnp  25292  limccnp2  25293  dvidlem  25316  dvn2bss  25331  cpnres  25338  dvcobr  25347  dvrec  25356  c1liplem1  25397  dvcnvrelem2  25419  dvfsumrlimf  25426  dvfsumlem1  25427  dvfsumlem2  25428  dvfsumlem3  25429  dvfsumlem4  25430  dvfsumrlim  25432  dvfsum2  25435  coeeulem  25622  coeid3  25638  plycn  25659  dvntaylp  25767  taylthlem1  25769  taylthlem2  25770  ulm2  25781  ulmshftlem  25785  ulmshft  25786  ulm0  25787  ulmcn  25795  ulmdvlem3  25798  ulmdv  25799  mtest  25800  mtestbdd  25801  dvradcnv  25817  psercn2  25819  psercn  25822  pserdv  25825  abelth  25837  efif1olem2  25936  efif1olem4  25938  efifo  25940  eff1olem  25941  logcn  26039  dvloglem  26040  cxpcn3  26138  resqrtcn  26139  sqrtcn  26140  logbleb  26170  logblt  26171  asinneg  26273  atanlogsub  26303  atanbnd  26313  ressatans  26321  leibpilem2  26328  xrlimcnp  26355  efrlim  26356  scvxcvx  26372  ppiub  26589  chtub  26597  logexprlim  26610  lgseisenlem1  26760  rplogsumlem1  26869  rplogsumlem2  26870  dchrisumlem2  26875  dchrisum0flb  26895  logdivbnd  26941  pntlem3  26994  tgcgr4  27536  ltgov  27602  f1otrg  27876  eengtrkg  27998  iedgedg  28064  ushgredgedgloop  28242  subgruhgredgd  28295  uvtxupgrres  28419  umgr2v2evd2  28538  edginwlk  28646  wlk1walk  28650  crctcshwlkn0lem6  28823  wlkiswwlks1  28875  minvecolem1  29879  minvecolem2  29880  minvecolem4  29885  htthlem  29922  5oalem2  30660  3oalem2  30668  iundisjf  31574  fmptco1f1o  31614  xppreima  31629  xppreima2  31634  dfcnv2  31659  gsumhashmul  31968  xrge0tsmsd  31969  odpmco  32007  pmtrcnelor  32012  pmtrto1cl  32018  psgnfzto1stlem  32019  fzto1stfv1  32020  fzto1st  32022  fzto1stinvn  32023  psgnfzto1st  32024  tocycf  32036  cycpmco2lem7  32051  cycpmco2  32052  cycpmrn  32062  cyc3evpm  32069  cyc3genpmlem  32070  cycpmgcl  32072  cyc3conja  32076  nsgmgc  32264  nsgqusf1olem1  32265  nsgqusf1olem2  32266  ghmqusker  32272  rhmpreimaprmidl  32300  ssmxidllem  32314  fply1  32341  ply1degltel  32365  ply1degltlss  32366  ply1degltdimlem  32404  ply1degltdim  32405  smatlem  32467  smatcl  32472  zartopn  32545  zarmxt1  32550  tpr2rico  32582  xrmulc1cn  32600  xrge0mulc1cn  32611  esumpfinvallem  32762  ldgenpisyslem1  32851  dynkin  32855  brfae  32936  sxbrsigalem3  32961  dya2icoseg2  32967  omsmeas  33012  sibfof  33029  sseqmw  33080  sseqf  33081  sseqp1  33084  fiblem  33087  fibp1  33090  probfinmeasbALTV  33118  repr0  33313  reprpmtf1o  33328  hgt750lemg  33356  bnj1379  33531  srcmpltd  33775  subfacp1lem5  33865  subfacp1lem6  33866  cvxpconn  33923  cvxsconn  33924  cvmliftlem6  33971  cvmliftlem8  33973  cvmliftlem10  33975  cvmlift2lem6  33989  cvmlift2lem11  33994  cvmlift2lem12  33995  2goelgoanfmla1  34105  prv1n  34112  msubff  34211  msubco  34212  elmsta  34229  msubff1  34237  mvhf  34239  msubvrs  34241  iprodefisumlem  34399  filnetlem3  34928  knoppcnlem10  35041  knoppcnlem11  35042  icoreunrn  35903  icoreelrn  35905  ralssiun  35951  poimirlem3  36154  poimirlem16  36167  poimirlem17  36168  poimirlem19  36170  poimirlem30  36181  dvasin  36235  cover2  36246  upixp  36261  sdclem1  36275  fdc  36277  caushft  36293  ismtyres  36340  rrncmslem  36364  isfld2  36537  osumcllem10N  38501  pexmidlem7N  38512  dihglblem2N  39830  lcfrvalsnN  40077  lcfrlem5  40082  lcfrlem6  40083  lcfrlem27  40105  lcfrlem37  40115  prjspvs  41006  0prjspnrel  41023  monotuz  41323  expdiophlem1  41403  kelac2  41450  naddwordnexlem4  41795  grurankcld  42635  dvgrat  42714  nzss  42719  uzmptshftfval  42748  binomcxplemnotnn0  42758  refsumcn  43357  rfcnpre2  43358  rfcnpre3  43360  rfcnpre4  43361  elabrexg  43371  disjf1o  43532  unirnmap  43550  unirnmapsn  43556  ssmapsn  43558  mptssid  43588  allbutfi  43748  eluzd  43764  uzidd2  43771  ressiocsup  43912  ressioosup  43913  ressiooinf  43915  fsumsermpt  43940  climexp  43966  climinf  43967  climsuse  43969  sumnnodd  43991  limsupresico  44061  limsupubuzlem  44073  limsupresxr  44127  liminfresxr  44128  liminfresico  44132  limsup10exlem  44133  cnrefiisplem  44190  cncfiooicclem1  44254  dvsinax  44274  itgsinexplem1  44315  fvvolioof  44350  fvvolicof  44352  stoweidlem14  44375  stoweidlem16  44377  stoweidlem31  44392  stoweidlem34  44395  stoweidlem36  44397  stoweidlem43  44404  stoweidlem46  44407  stoweidlem47  44408  stoweidlem52  44413  stoweidlem55  44416  stoweidlem57  44418  dirkercncf  44468  fourierdlem20  44488  fourierdlem42  44510  fourierdlem48  44515  fourierdlem49  44516  fourierdlem51  44518  fourierdlem54  44521  fourierdlem62  44529  fourierdlem71  44538  fourierdlem80  44547  fourierdlem114  44581  fouriersw  44592  ioorrnopnlem  44665  ioorrnopnxrlem  44667  salexct3  44703  salgencntex  44704  salgensscntex  44705  subsalsal  44720  sge0fodjrnlem  44777  sge0isum  44788  sge0seq  44807  sge0reuz  44808  sge0reuzb  44809  meadjiunlem  44826  meaiininclem  44847  carageniuncllem1  44882  caratheodorylem1  44887  hoiprodp1  44949  hoidmv1lelem1  44952  hoidmv1lelem2  44953  hoidmv1le  44955  hoidmvlelem1  44956  hoidmvlelem2  44957  hoidmvlelem3  44958  voncmpl  44982  hoiqssbl  44986  smflimlem2  45133  smfsuplem1  45172  smfsuplem3  45174  fsupdm  45203  finfdm  45207  cfsetsnfsetf  45412  fcores  45421  afvres  45524  afv2res  45591  fundcmpsurinjimaid  45723  iccpartigtl  45735  sprsymrelf  45807  prproropf1olem2  45816  ushrisomgr  46153  funcringcsetcALTV2lem3  46456  funcringcsetclem3ALTV  46479  lindslinindsimp2lem5  46663  rrxsphere  46954  line2  46958  iooii  47070  icccldii  47071  iscnrm3rlem3  47095  onsetreclem3  47272  amgmwlem  47369