Theorem ssel2 3932

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

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

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 2803  df-ss 3922

This theorem is referenced by:  tz7.7  6337  onfr  6350  onmindif  6405  ordunisssuc  6419  ssimaex  6912  nssdmovg  7535  onnmin  7738  onmindif2  7747  limsssuc  7790  el2xpss  7979  1st2nd  7981  f1o2ndf1  8062  dfrecs3  8302  boxriin  8874  ordunifi  9195  isfinite2  9203  ordtypelem7  9435  sucprcreg  9515  cnfcom  9615  eldju1st  9838  coflim  10174  cflim2  10176  fin23lem11  10230  fin23lem26  10238  fin1a2lem13  10325  fpwwe2lem11  10554  suplem2pr  10966  axpre-sup  11082  axsup  11209  dedekind  11297  dedekindle  11298  fimaxre  12087  fiminre  12090  lbinf  12096  dfinfre  12124  infrelb  12128  suprfinzcl  12608  uzwo  12830  supminf  12854  lbzbi  12855  zsupss  12856  suprzcl2  12857  xrsupsslem  13227  xrinfmsslem  13228  xrub  13232  supxr2  13234  supxrun  13236  supxrunb1  13239  supxrbnd1  13241  supxrbnd2  13242  supxrub  13244  supxrbnd  13248  infxrlb  13255  elfzom1elp1fzo  13653  ssfzo12  13680  fsuppmapnn0fiublem  13915  fsuppmapnn0fiub  13916  fsuppmapnn0fiub0  13918  seqsplit  13960  shftlem  14993  rpnnen2lem10  16150  rpnnen2lem11  16151  gcdcllem1  16428  mrcuni  17545  isacs1i  17581  mreacs  17582  lubss  18437  gsumwspan  18738  subgint  19047  cntziinsn  19234  cntzsubg  19236  pmtrdifellem4  19376  subrngint  20463  cntzsubrng  20470  subrgint  20498  cntzsubr  20509  sraassab  21793  mdetunilem9  22523  tgcl  22872  fctop  22907  cctop  22909  neips  23016  cmpsub  23303  1stcelcls  23364  ssref  23415  comppfsc  23435  txbasval  23509  fgss2  23777  filconn  23786  filuni  23788  filssufilg  23814  fmfnfmlem4  23860  trust  24133  elmopn2  24349  metrest  24428  dscopn  24477  metds0  24755  cncfmet  24818  negcncf  24831  negcncfOLD  24832  iscmet2  25210  ovolfioo  25384  ovolficc  25385  itg1mulc  25621  ply1term  26125  plyconst  26127  reeff1olem  26372  nosupno  27631  nosupbday  27633  nosupbnd1lem5  27640  noinfno  27646  noinfbday  27648  noetasuplem4  27664  n0sfincut  28269  usgruspgrb  29146  ocsh  31245  ocorth  31253  spansncvi  31614  pjss1coi  32125  sumdmdii  32377  unidifsnel  32497  dfcnv2  32633  xrge0infss  32716  measdivcst  34193  measdivcstALTV  34194  dya2iocuni  34253  bnj1190  34977  nummin  35060  opnrebl  36296  opnrebl2  36297  fness  36325  nlpineqsn  37384  fin2so  37589  matunitlindflem1  37598  poimirlem27  37629  poimir  37635  frinfm  37717  filbcmb  37722  nnubfi  37732  nninfnub  37733  sstotbnd3  37758  bndss  37768  exidreslem  37859  isidlc  37997  idlnegcl  38004  intidl  38011  unichnidl  38013  pmapglb2N  39753  elpaddn0  39782  paddasslem9  39810  paddasslem10  39811  pclfinN  39882  polval2N  39888  diaglbN  41037  dihord6apre  41238  unielss  43194  onmaxnelsup  43199  onsupmaxb  43215  onsupeqnmax  43223  gneispace  44110  snsslVD  44805  snssl  44806  sstrALT2VD  44810  sstrALT2  44811  suctrALTcf  44898  suctrALTcfVD  44899  ssnel  45024  uzwo4  45034  infxrunb2  45351  infxrbnd2  45352  supxrunb3  45382  unb2ltle  45398  infxrpnf  45429  supminfxr  45447  sge0iunmptlemfi  46398  caratheodorylem2  46512  ovnlerp  46547  ssfz12  47302  prssspr  47473  prsssprel  47476  lindslinindimp2lem4  48450  lindslinindsimp2  48452  lincresunit3lem2  48469  lincresunit3  48470