Theorem ssel2 4003

Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 7-Jun-2004.)

Assertion

Ref	Expression
ssel2	⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵)

Proof of Theorem ssel2

Step	Hyp	Ref	Expression
1		ssel 4002	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
2	1	imp 406	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-clel 2819  df-ss 3993

This theorem is referenced by:  tz7.7  6421  onfr  6434  onmindif  6487  ordunisssuc  6501  ssimaex  7007  nssdmovg  7632  onnmin  7834  onmindif2  7843  limsssuc  7887  el2xpss  8078  1st2nd  8080  f1o2ndf1  8163  dfrecs3  8428  dfrecs3OLD  8429  boxriin  8998  ordunifi  9354  isfinite2  9362  ordtypelem7  9593  sucprcreg  9670  cnfcom  9769  eldju1st  9992  coflim  10330  cflim2  10332  fin23lem11  10386  fin23lem26  10394  fin1a2lem13  10481  fpwwe2lem11  10710  suplem2pr  11122  axpre-sup  11238  axsup  11365  dedekind  11453  dedekindle  11454  fimaxre  12239  fiminre  12242  lbinf  12248  dfinfre  12276  infrelb  12280  suprfinzcl  12757  uzwo  12976  supminf  13000  lbzbi  13001  zsupss  13002  suprzcl2  13003  xrsupsslem  13369  xrinfmsslem  13370  xrub  13374  supxr2  13376  supxrun  13378  supxrunb1  13381  supxrbnd1  13383  supxrbnd2  13384  supxrub  13386  supxrbnd  13390  infxrlb  13396  elfzom1elp1fzo  13783  ssfzo12  13809  fsuppmapnn0fiublem  14041  fsuppmapnn0fiub  14042  fsuppmapnn0fiub0  14044  seqsplit  14086  shftlem  15117  rpnnen2lem10  16271  rpnnen2lem11  16272  gcdcllem1  16545  mrcuni  17679  isacs1i  17715  mreacs  17716  lubss  18583  gsumwspan  18881  subgint  19190  cntziinsn  19377  cntzsubg  19379  pmtrdifellem4  19521  subrngint  20586  cntzsubrng  20593  subrgint  20623  cntzsubr  20634  sraassab  21911  mdetunilem9  22647  tgcl  22997  fctop  23032  cctop  23034  neips  23142  cmpsub  23429  1stcelcls  23490  ssref  23541  comppfsc  23561  txbasval  23635  fgss2  23903  filconn  23912  filuni  23914  filssufilg  23940  fmfnfmlem4  23986  trust  24259  elmopn2  24476  metrest  24558  dscopn  24607  metds0  24891  cncfmet  24954  negcncf  24967  negcncfOLD  24968  iscmet2  25347  ovolfioo  25521  ovolficc  25522  itg1mulc  25759  ply1term  26263  plyconst  26265  reeff1olem  26508  nosupno  27766  nosupbday  27768  nosupbnd1lem5  27775  noinfno  27781  noinfbday  27783  noetasuplem4  27799  usgruspgrb  29218  ocsh  31315  ocorth  31323  spansncvi  31684  pjss1coi  32195  sumdmdii  32447  unidifsnel  32563  dfcnv2  32694  xrge0infss  32767  measdivcst  34188  measdivcstALTV  34189  dya2iocuni  34248  bnj1190  34984  nummin  35067  opnrebl  36286  opnrebl2  36287  fness  36315  nlpineqsn  37374  fin2so  37567  matunitlindflem1  37576  poimirlem27  37607  poimir  37613  frinfm  37695  filbcmb  37700  nnubfi  37710  nninfnub  37711  sstotbnd3  37736  bndss  37746  exidreslem  37837  isidlc  37975  idlnegcl  37982  intidl  37989  unichnidl  37991  pmapglb2N  39728  elpaddn0  39757  paddasslem9  39785  paddasslem10  39786  pclfinN  39857  polval2N  39863  diaglbN  41012  dihord6apre  41213  unielss  43179  onmaxnelsup  43184  onsupmaxb  43200  onsupeqnmax  43208  gneispace  44096  snsslVD  44800  snssl  44801  sstrALT2VD  44805  sstrALT2  44806  suctrALTcf  44893  suctrALTcfVD  44894  ssnel  44943  uzwo4  44955  infxrunb2  45283  infxrbnd2  45284  supxrunb3  45314  unb2ltle  45330  infxrpnf  45361  supminfxr  45379  sge0iunmptlemfi  46334  caratheodorylem2  46448  ovnlerp  46483  ssfz12  47229  prssspr  47359  prsssprel  47362  lindslinindimp2lem4  48190  lindslinindsimp2  48192  lincresunit3lem2  48209  lincresunit3  48210