Theorem ssel2 3941

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

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

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 3931

This theorem is referenced by:  tz7.7  6358  onfr  6371  onmindif  6426  ordunisssuc  6440  ssimaex  6946  nssdmovg  7571  onnmin  7774  onmindif2  7783  limsssuc  7826  el2xpss  8016  1st2nd  8018  f1o2ndf1  8101  dfrecs3  8341  boxriin  8913  ordunifi  9237  isfinite2  9245  ordtypelem7  9477  sucprcreg  9554  cnfcom  9653  eldju1st  9876  coflim  10214  cflim2  10216  fin23lem11  10270  fin23lem26  10278  fin1a2lem13  10365  fpwwe2lem11  10594  suplem2pr  11006  axpre-sup  11122  axsup  11249  dedekind  11337  dedekindle  11338  fimaxre  12127  fiminre  12130  lbinf  12136  dfinfre  12164  infrelb  12168  suprfinzcl  12648  uzwo  12870  supminf  12894  lbzbi  12895  zsupss  12896  suprzcl2  12897  xrsupsslem  13267  xrinfmsslem  13268  xrub  13272  supxr2  13274  supxrun  13276  supxrunb1  13279  supxrbnd1  13281  supxrbnd2  13282  supxrub  13284  supxrbnd  13288  infxrlb  13295  elfzom1elp1fzo  13693  ssfzo12  13720  fsuppmapnn0fiublem  13955  fsuppmapnn0fiub  13956  fsuppmapnn0fiub0  13958  seqsplit  14000  shftlem  15034  rpnnen2lem10  16191  rpnnen2lem11  16192  gcdcllem1  16469  mrcuni  17582  isacs1i  17618  mreacs  17619  lubss  18472  gsumwspan  18773  subgint  19082  cntziinsn  19269  cntzsubg  19271  pmtrdifellem4  19409  subrngint  20469  cntzsubrng  20476  subrgint  20504  cntzsubr  20515  sraassab  21777  mdetunilem9  22507  tgcl  22856  fctop  22891  cctop  22893  neips  23000  cmpsub  23287  1stcelcls  23348  ssref  23399  comppfsc  23419  txbasval  23493  fgss2  23761  filconn  23770  filuni  23772  filssufilg  23798  fmfnfmlem4  23844  trust  24117  elmopn2  24333  metrest  24412  dscopn  24461  metds0  24739  cncfmet  24802  negcncf  24815  negcncfOLD  24816  iscmet2  25194  ovolfioo  25368  ovolficc  25369  itg1mulc  25605  ply1term  26109  plyconst  26111  reeff1olem  26356  nosupno  27615  nosupbday  27617  nosupbnd1lem5  27624  noinfno  27630  noinfbday  27632  noetasuplem4  27648  n0sfincut  28246  usgruspgrb  29110  ocsh  31212  ocorth  31220  spansncvi  31581  pjss1coi  32092  sumdmdii  32344  unidifsnel  32464  dfcnv2  32600  xrge0infss  32683  measdivcst  34214  measdivcstALTV  34215  dya2iocuni  34274  bnj1190  34998  nummin  35081  opnrebl  36308  opnrebl2  36309  fness  36337  nlpineqsn  37396  fin2so  37601  matunitlindflem1  37610  poimirlem27  37641  poimir  37647  frinfm  37729  filbcmb  37734  nnubfi  37744  nninfnub  37745  sstotbnd3  37770  bndss  37780  exidreslem  37871  isidlc  38009  idlnegcl  38016  intidl  38023  unichnidl  38025  pmapglb2N  39765  elpaddn0  39794  paddasslem9  39822  paddasslem10  39823  pclfinN  39894  polval2N  39900  diaglbN  41049  dihord6apre  41250  unielss  43207  onmaxnelsup  43212  onsupmaxb  43228  onsupeqnmax  43236  gneispace  44123  snsslVD  44818  snssl  44819  sstrALT2VD  44823  sstrALT2  44824  suctrALTcf  44911  suctrALTcfVD  44912  ssnel  45037  uzwo4  45047  infxrunb2  45364  infxrbnd2  45365  supxrunb3  45395  unb2ltle  45411  infxrpnf  45442  supminfxr  45460  sge0iunmptlemfi  46411  caratheodorylem2  46525  ovnlerp  46560  ssfz12  47315  prssspr  47486  prsssprel  47489  lindslinindimp2lem4  48450  lindslinindsimp2  48452  lincresunit3lem2  48469  lincresunit3  48470