Theorem ssel2 3958

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 3957	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
2	1	imp 406	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2810  df-ss 3948

This theorem is referenced by:  tz7.7  6383  onfr  6396  onmindif  6451  ordunisssuc  6465  ssimaex  6969  nssdmovg  7594  onnmin  7797  onmindif2  7806  limsssuc  7850  el2xpss  8041  1st2nd  8043  f1o2ndf1  8126  dfrecs3  8391  dfrecs3OLD  8392  boxriin  8959  ordunifi  9303  isfinite2  9311  ordtypelem7  9543  sucprcreg  9620  cnfcom  9719  eldju1st  9942  coflim  10280  cflim2  10282  fin23lem11  10336  fin23lem26  10344  fin1a2lem13  10431  fpwwe2lem11  10660  suplem2pr  11072  axpre-sup  11188  axsup  11315  dedekind  11403  dedekindle  11404  fimaxre  12191  fiminre  12194  lbinf  12200  dfinfre  12228  infrelb  12232  suprfinzcl  12712  uzwo  12932  supminf  12956  lbzbi  12957  zsupss  12958  suprzcl2  12959  xrsupsslem  13328  xrinfmsslem  13329  xrub  13333  supxr2  13335  supxrun  13337  supxrunb1  13340  supxrbnd1  13342  supxrbnd2  13343  supxrub  13345  supxrbnd  13349  infxrlb  13356  elfzom1elp1fzo  13753  ssfzo12  13780  fsuppmapnn0fiublem  14013  fsuppmapnn0fiub  14014  fsuppmapnn0fiub0  14016  seqsplit  14058  shftlem  15092  rpnnen2lem10  16246  rpnnen2lem11  16247  gcdcllem1  16523  mrcuni  17638  isacs1i  17674  mreacs  17675  lubss  18528  gsumwspan  18829  subgint  19138  cntziinsn  19325  cntzsubg  19327  pmtrdifellem4  19465  subrngint  20525  cntzsubrng  20532  subrgint  20560  cntzsubr  20571  sraassab  21833  mdetunilem9  22563  tgcl  22912  fctop  22947  cctop  22949  neips  23056  cmpsub  23343  1stcelcls  23404  ssref  23455  comppfsc  23475  txbasval  23549  fgss2  23817  filconn  23826  filuni  23828  filssufilg  23854  fmfnfmlem4  23900  trust  24173  elmopn2  24389  metrest  24468  dscopn  24517  metds0  24795  cncfmet  24858  negcncf  24871  negcncfOLD  24872  iscmet2  25251  ovolfioo  25425  ovolficc  25426  itg1mulc  25662  ply1term  26166  plyconst  26168  reeff1olem  26413  nosupno  27672  nosupbday  27674  nosupbnd1lem5  27681  noinfno  27687  noinfbday  27689  noetasuplem4  27705  n0sfincut  28303  usgruspgrb  29167  ocsh  31269  ocorth  31277  spansncvi  31638  pjss1coi  32149  sumdmdii  32401  unidifsnel  32521  dfcnv2  32659  xrge0infss  32742  measdivcst  34260  measdivcstALTV  34261  dya2iocuni  34320  bnj1190  35044  nummin  35127  opnrebl  36343  opnrebl2  36344  fness  36372  nlpineqsn  37431  fin2so  37636  matunitlindflem1  37645  poimirlem27  37676  poimir  37682  frinfm  37764  filbcmb  37769  nnubfi  37779  nninfnub  37780  sstotbnd3  37805  bndss  37815  exidreslem  37906  isidlc  38044  idlnegcl  38051  intidl  38058  unichnidl  38060  pmapglb2N  39795  elpaddn0  39824  paddasslem9  39852  paddasslem10  39853  pclfinN  39924  polval2N  39930  diaglbN  41079  dihord6apre  41280  unielss  43217  onmaxnelsup  43222  onsupmaxb  43238  onsupeqnmax  43246  gneispace  44133  snsslVD  44828  snssl  44829  sstrALT2VD  44833  sstrALT2  44834  suctrALTcf  44921  suctrALTcfVD  44922  ssnel  45047  uzwo4  45057  infxrunb2  45375  infxrbnd2  45376  supxrunb3  45406  unb2ltle  45422  infxrpnf  45453  supminfxr  45471  sge0iunmptlemfi  46422  caratheodorylem2  46536  ovnlerp  46571  ssfz12  47323  prssspr  47479  prsssprel  47482  lindslinindimp2lem4  48417  lindslinindsimp2  48419  lincresunit3lem2  48436  lincresunit3  48437