Theorem ssel2 3929

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-clel 2836  df-ss 3919

This theorem is referenced by:  tz7.7  6367  onfr  6380  onmindif  6435  ordunisssuc  6449  ssimaex  6947  nssdmovg  7573  onnmin  7776  onmindif2  7785  limsssuc  7825  el2xpss  8013  1st2nd  8015  f1o2ndf1  8095  dfrecs3  8337  boxriin  8916  ordunifi  9228  isfinite2  9236  ordtypelem7  9466  sucprcregOLD  9549  cnfcom  9649  eldju1st  9875  coflim  10212  cflim2  10214  fin23lem11  10268  fin23lem26  10276  fin1a2lem13  10363  fpwwe2lem11  10593  suplem2pr  11005  axpre-sup  11121  axsup  11252  dedekind  11340  dedekindle  11341  fimaxre  12130  fiminre  12133  lbinf  12139  dfinfre  12167  infrelb  12171  suprfinzcl  12681  uzwo  12906  supminf  12930  lbzbi  12931  zsupss  12932  suprzcl2  12933  xrsupsslem  13304  xrinfmsslem  13305  xrub  13309  supxr2  13311  supxrun  13313  supxrunb1  13316  supxrbnd1  13318  supxrbnd2  13319  supxrub  13321  supxrbnd  13325  infxrlb  13332  elfzom1elp1fzo  13732  ssfzo12  13759  fsuppmapnn0fiublem  13997  fsuppmapnn0fiub  13998  fsuppmapnn0fiub0  14000  seqsplit  14042  shftlem  15075  rpnnen2lem10  16246  rpnnen2lem11  16247  gcdcllem1  16524  mrcuni  17644  isacs1i  17680  mreacs  17681  lubss  18536  gsumwspan  18871  subgint  19183  cntziinsn  19368  cntzsubg  19370  pmtrdifellem4  19510  subrngint  20597  cntzsubrng  20604  subrgint  20632  cntzsubr  20643  sraassab  21908  mdetunilem9  22668  tgcl  23017  fctop  23052  cctop  23054  neips  23161  cmpsub  23448  1stcelcls  23509  ssref  23560  comppfsc  23580  txbasval  23654  fgss2  23922  filconn  23931  filuni  23933  filssufilg  23959  fmfnfmlem4  24005  trust  24277  elmopn2  24493  metrest  24572  dscopn  24621  metds0  24899  cncfmet  24959  negcncf  24972  iscmet2  25344  ovolfioo  25517  ovolficc  25518  itg1mulc  25754  ply1term  26252  plyconst  26254  reeff1olem  26497  nosupno  27755  nosupbday  27757  nosupbnd1lem5  27764  noinfno  27770  noinfbday  27772  noetasuplem4  27788  n0fincut  28436  usgruspgrb  29341  ocsh  31443  ocorth  31451  spansncvi  31812  pjss1coi  32323  sumdmdii  32575  unidifsnel  32694  dfcnv2  32838  xrge0infss  32923  measdivcst  34482  measdivcstALTV  34483  dya2iocuni  34541  bnj1190  35264  nummin  35350  trssfir1om  35368  trssfir1omregs  35393  opnrebl  36641  opnrebl2  36642  fness  36670  ttcmin  36817  nlpineqsn  37863  fin2so  38067  matunitlindflem1  38076  poimirlem27  38107  poimir  38113  frinfm  38195  filbcmb  38200  nnubfi  38210  nninfnub  38211  sstotbnd3  38236  bndss  38246  exidreslem  38337  isidlc  38475  idlnegcl  38482  intidl  38489  unichnidl  38491  pmapglb2N  40356  elpaddn0  40385  paddasslem9  40413  paddasslem10  40414  pclfinN  40485  polval2N  40491  diaglbN  41640  dihord6apre  41841  unielss  43756  onmaxnelsup  43761  onsupmaxb  43777  onsupeqnmax  43785  gneispace  44671  snsslVD  45365  snssl  45366  sstrALT2VD  45370  sstrALT2  45371  suctrALTcf  45458  suctrALTcfVD  45459  ssnel  45584  uzwo4  45594  infxrunb2  45904  infxrbnd2  45905  supxrunb3  45935  unb2ltle  45950  infxrpnf  45981  supminfxr  45999  sge0iunmptlemfi  46948  caratheodorylem2  47062  ovnlerp  47097  ssfz12  47869  prssspr  48052  prsssprel  48055  lindslinindimp2lem4  49044  lindslinindsimp2  49046  lincresunit3lem2  49063  lincresunit3  49064