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 1540   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

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

This theorem is referenced by:  3eltr4g  2849  brelrng  5940  elabrex  7244  elabrexg  7245  fliftel1  7310  ovidig  7553  unielxp  8017  tfrlem11  8392  rdglim  8430  seqomlem4  8457  2oconcl  8507  ecopqsi  8772  erov  8812  eroprf  8813  sbthlem2  9088  dffi3  9430  ixpiunwdom  9589  cantnfcl  9666  r1lim  9771  rankwflemb  9792  pwwf  9806  unwf  9809  rankwflem  9814  uniwf  9818  rankpwi  9822  rankr1g  9831  r1pw  9844  r1rankid  9858  rankuni  9862  djulcl  9909  djurcl  9910  inlresf  9913  inrresf  9915  djuun  9925  cardlim  9971  infxpenlem  10012  alephfp  10107  cfsmolem  10269  alephsing  10275  hsmexlem4  10428  axdc3lem2  10450  numth3  10469  iunfo  10538  konigthlem  10567  iunctb  10573  canthwelem  10649  canthwe  10650  r1limwun  10735  inar1  10774  inatsk  10777  gruina  10817  grur1  10819  tskmval  10838  tskmcl  10840  pinq  10926  dmrecnq  10967  addclsr  11082  mulclsr  11083  axaddf  11144  axmulf  11145  peano2nn  12229  uztrn2  12846  eluz2nn  12873  peano2uzs  12891  uzsupss  12929  uzsup  13833  uzrdgfni  13928  uzrdgsuci  13930  fsuppmapnn0fiub  13961  seqf  13994  ser0  14025  bcm1k  14280  bcp1nk  14282  bcpasc  14286  hashprdifel  14363  fz1isolem  14427  pr2pwpr  14445  ccats1val2  14582  rexuzre  15304  limsupgre  15430  climconst  15492  rlimclim1  15494  climrlim2  15496  clim2ser  15606  clim2ser2  15607  iserex  15608  isermulc2  15609  iserle  15611  isercolllem3  15618  isercoll2  15620  climsup  15621  iseraltlem2  15634  iseraltlem3  15635  zsum  15669  isumclim3  15710  isumadd  15718  fsump1i  15720  iserabs  15766  cvgcmp  15767  cvgcmpub  15768  cvgcmpce  15769  abscvgcvg  15770  isumshft  15790  isumsplit  15791  isum1p  15792  isumrpcl  15794  isumsup2  15797  climcndslem1  15800  cvgrat  15834  clim2prod  15839  clim2div  15840  prodf1  15842  ntrivcvgn0  15849  ntrivcvgtail  15851  fprodntriv  15891  fprodabs  15923  fprodeq0  15924  iprodclim3  15949  iprodmul  15952  ef0lem  16027  fprodefsum  16043  rpnnen2lem3  16164  dvdsflip  16265  fzo0dvdseq  16271  bitsinv1  16388  smupval  16434  smueqlem  16436  seq1st  16513  algr0  16514  prmind2  16627  crth  16716  eulerthlem2  16720  prmdiv  16723  pockthlem  16843  pockthg  16844  unbenlem  16846  prmunb  16852  prmgaplem7  16995  strfv2d  17140  imasvscaval  17489  oppccatid  17670  oppccatf  17679  epii  17695  fthepi  17884  funcestrcsetclem3  18099  funcsetcestrclem3  18113  yon12  18223  yon2  18224  yonedalem4c  18235  yonedalem22  18236  yonedalem3b  18237  yonedainv  18239  acsmapd  18512  mgm2nsgrplem1  18836  mgm2nsgrplem2  18837  mgm2nsgrplem3  18838  sgrp2nmndlem1  18841  sgrp2rid2  18844  cntrsubgnsg  19249  symgpssefmnd  19305  pmtrrn  19367  gexcl3  19497  efgi  19629  efgi2  19635  efgs1b  19646  efgredlemg  19652  efgredlemd  19654  frgpnabllem1  19783  cycsubgcyg  19811  gsumzaddlem  19831  dprdwd  19923  dprd2da  19954  rhmopp  20401  lsppratlem3  20908  lsppratlem4  20909  lbsextlem2  20918  lidl0  20994  lidl1  20995  2idl0  21013  2idl1  21014  domnchr  21304  znf1o  21327  mplsubrglem  21783  mpfconst  21884  mpfproj  21885  mpfind  21890  mhpmulcl  21912  pf1const  22086  pf1id  22087  mpfpf1  22091  pf1mpf  22092  madetsumid  22184  slesolex  22405  pmatcoe1fsupp  22424  mat2pmatbas0  22450  pmatcollpw  22504  pm2mpf1  22522  isclo  22812  indiscld  22816  restntr  22907  ordtbaslem  22913  ordtbas2  22916  lmconst  22986  lmss  23023  conncompid  23156  2ndcomap  23183  locfincmp  23251  comppfsc  23257  xkouni  23324  txcls  23329  ptclsg  23340  uptx  23350  txindis  23359  tx1stc  23375  cnmpt1res  23401  tgqtop  23437  uffix  23646  cnpflf2  23725  ptcmplem2  23778  ptcmplem4  23780  tgpconncomp  23838  tsmsfbas  23853  fmucnd  24018  prdsxmetlem  24095  imasdsf1olem  24100  prdsbl  24221  blcvx  24535  xrsmopn  24549  xrge0tsms  24571  metdcn2  24576  expcncf  24668  cnmpopc  24670  icchmeo  24686  icchmeoOLD  24687  iccpnfhmeo  24691  cnheibor  24702  evth  24706  evth2  24707  lebnumlem2  24709  lebnumii  24713  reparphti  24744  reparphtiOLD  24745  cfilfcls  25023  minveclem2  25175  minveclem3  25178  minveclem4  25181  ovoliunlem1  25252  ovolicc1  25266  iundisj  25298  volsup  25306  uniioombllem3  25335  vitalilem2  25359  vitalilem3  25360  mbfsup  25414  mbfinf  25415  mbflimsup  25416  itg2monolem1  25501  limcflflem  25630  limccnp  25641  limccnp2  25642  dvidlem  25665  dvn2bss  25681  cpnres  25688  dvcobr  25698  dvcobrOLD  25699  dvrec  25708  c1liplem1  25749  dvcnvrelem2  25771  dvfsumrlimf  25778  dvfsumlem1  25779  dvfsumlem2  25780  dvfsumlem3  25781  dvfsumlem4  25782  dvfsumrlim  25784  dvfsum2  25787  coeeulem  25974  coeid3  25990  plycn  26011  plycnOLD  26012  dvntaylp  26120  taylthlem1  26122  taylthlem2  26123  ulm2  26134  ulmshftlem  26138  ulmshft  26139  ulm0  26140  ulmcn  26148  ulmdvlem3  26151  ulmdv  26152  mtest  26153  mtestbdd  26154  dvradcnv  26170  psercn2  26172  psercn  26175  pserdv  26178  abelth  26190  efif1olem2  26289  efif1olem4  26291  efifo  26293  eff1olem  26294  logcn  26392  dvloglem  26393  cxpcn3  26493  resqrtcn  26494  sqrtcn  26495  logbleb  26525  logblt  26526  asinneg  26628  atanlogsub  26658  atanbnd  26668  ressatans  26676  leibpilem2  26683  xrlimcnp  26710  efrlim  26711  scvxcvx  26727  ppiub  26944  chtub  26952  logexprlim  26965  lgseisenlem1  27115  rplogsumlem1  27224  rplogsumlem2  27225  dchrisumlem2  27230  dchrisum0flb  27250  logdivbnd  27296  pntlem3  27349  peano2n0s  27941  tgcgr4  28050  ltgov  28116  f1otrg  28390  eengtrkg  28512  iedgedg  28578  ushgredgedgloop  28756  subgruhgredgd  28809  uvtxupgrres  28933  umgr2v2evd2  29052  edginwlk  29160  wlk1walk  29164  crctcshwlkn0lem6  29337  wlkiswwlks1  29389  minvecolem1  30395  minvecolem2  30396  minvecolem4  30401  htthlem  30438  5oalem2  31176  3oalem2  31184  iundisjf  32088  fmptco1f1o  32125  xppreima  32139  xppreima2  32144  dfcnv2  32169  gsumhashmul  32479  xrge0tsmsd  32480  odpmco  32518  pmtrcnelor  32523  pmtrto1cl  32529  psgnfzto1stlem  32530  fzto1stfv1  32531  fzto1st  32533  fzto1stinvn  32534  psgnfzto1st  32535  tocycf  32547  cycpmco2lem7  32562  cycpmco2  32563  cycpmrn  32573  cyc3evpm  32580  cyc3genpmlem  32581  cycpmgcl  32583  cyc3conja  32587  nsgmgc  32798  nsgqusf1olem1  32799  nsgqusf1olem2  32800  ghmqusker  32807  rhmpreimaprmidl  32845  ssmxidllem  32864  opprqus1r  32881  qsdrngilem  32883  qsdrngi  32884  fply1  32912  ply1degltel  32941  ply1degleel  32942  ply1degltlss  32943  ply1degltdimlem  32996  ply1degltdim  32997  algextdeglem4  33066  algextdeglem6  33068  algextdeglem7  33069  algextdeglem8  33070  smatlem  33076  smatcl  33081  zartopn  33154  zarmxt1  33159  tpr2rico  33191  xrmulc1cn  33209  xrge0mulc1cn  33220  esumpfinvallem  33371  ldgenpisyslem1  33460  dynkin  33464  brfae  33545  sxbrsigalem3  33570  dya2icoseg2  33576  omsmeas  33621  sibfof  33638  sseqmw  33689  sseqf  33690  sseqp1  33693  fiblem  33696  fibp1  33699  probfinmeasbALTV  33727  repr0  33922  reprpmtf1o  33937  hgt750lemg  33965  bnj1379  34140  srcmpltd  34384  subfacp1lem5  34474  subfacp1lem6  34475  cvxpconn  34532  cvxsconn  34533  cvmliftlem6  34580  cvmliftlem8  34582  cvmliftlem10  34584  cvmlift2lem6  34598  cvmlift2lem11  34603  cvmlift2lem12  34604  2goelgoanfmla1  34714  prv1n  34721  msubff  34820  msubco  34821  elmsta  34838  msubff1  34846  mvhf  34848  msubvrs  34850  iprodefisumlem  35015  gg-psercn2  35465  gg-dvfsumlem2  35470  filnetlem3  35569  knoppcnlem10  35682  knoppcnlem11  35683  icoreunrn  36544  icoreelrn  36546  ralssiun  36592  poimirlem3  36795  poimirlem16  36808  poimirlem17  36809  poimirlem19  36811  poimirlem30  36822  dvasin  36876  cover2  36887  upixp  36901  sdclem1  36915  fdc  36917  caushft  36933  ismtyres  36980  rrncmslem  37004  isfld2  37177  osumcllem10N  39140  pexmidlem7N  39151  dihglblem2N  40469  lcfrvalsnN  40716  lcfrlem5  40721  lcfrlem6  40722  lcfrlem27  40744  lcfrlem37  40754  prjspvs  41655  0prjspnrel  41672  monotuz  41983  expdiophlem1  42063  kelac2  42110  naddwordnexlem4  42455  grurankcld  43295  dvgrat  43374  nzss  43379  uzmptshftfval  43408  binomcxplemnotnn0  43418  refsumcn  44017  rfcnpre2  44018  rfcnpre3  44020  rfcnpre4  44021  disjf1o  44189  unirnmap  44206  unirnmapsn  44212  ssmapsn  44214  mptssid  44243  allbutfi  44402  eluzd  44418  uzidd2  44425  ressiocsup  44566  ressioosup  44567  ressiooinf  44569  fsumsermpt  44594  climexp  44620  climinf  44621  climsuse  44623  sumnnodd  44645  limsupresico  44715  limsupubuzlem  44727  limsupresxr  44781  liminfresxr  44782  liminfresico  44786  limsup10exlem  44787  cnrefiisplem  44844  cncfiooicclem1  44908  dvsinax  44928  itgsinexplem1  44969  fvvolioof  45004  fvvolicof  45006  stoweidlem14  45029  stoweidlem16  45031  stoweidlem31  45046  stoweidlem34  45049  stoweidlem36  45051  stoweidlem43  45058  stoweidlem46  45061  stoweidlem47  45062  stoweidlem52  45067  stoweidlem55  45070  stoweidlem57  45072  dirkercncf  45122  fourierdlem20  45142  fourierdlem42  45164  fourierdlem48  45169  fourierdlem49  45170  fourierdlem51  45172  fourierdlem54  45175  fourierdlem62  45183  fourierdlem71  45192  fourierdlem80  45201  fourierdlem114  45235  fouriersw  45246  ioorrnopnlem  45319  ioorrnopnxrlem  45321  salexct3  45357  salgencntex  45358  salgensscntex  45359  subsalsal  45374  sge0fodjrnlem  45431  sge0isum  45442  sge0seq  45461  sge0reuz  45462  sge0reuzb  45463  meadjiunlem  45480  meaiininclem  45501  carageniuncllem1  45536  caratheodorylem1  45541  hoiprodp1  45603  hoidmv1lelem1  45606  hoidmv1lelem2  45607  hoidmv1le  45609  hoidmvlelem1  45610  hoidmvlelem2  45611  hoidmvlelem3  45612  voncmpl  45636  hoiqssbl  45640  smflimlem2  45787  smfsuplem1  45826  smfsuplem3  45828  fsupdm  45857  finfdm  45861  cfsetsnfsetf  46067  fcores  46076  afvres  46179  afv2res  46246  fundcmpsurinjimaid  46378  iccpartigtl  46390  sprsymrelf  46462  prproropf1olem2  46471  ushrisomgr  46808  funcringcsetcALTV2lem3  47025  funcringcsetclem3ALTV  47048  lindslinindsimp2lem5  47231  rrxsphere  47522  line2  47526  iooii  47638  icccldii  47639  iscnrm3rlem3  47663  onsetreclem3  47840  amgmwlem  47937