Theorem ssel2 3927

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2105   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3443  df-in 3905  df-ss 3915

This theorem is referenced by:  tz7.7  6329  onfr  6342  onmindif  6394  ordunisssuc  6407  ssimaex  6910  nssdmovg  7517  onnmin  7712  onmindif2  7721  limsssuc  7765  1st2nd  7949  f1o2ndf1  8031  dfrecs3  8274  dfrecs3OLD  8275  boxriin  8800  ordunifi  9159  isfinite2  9167  ordtypelem7  9382  sucprcreg  9459  cnfcom  9558  eldju1st  9781  coflim  10119  cflim2  10121  fin23lem11  10175  fin23lem26  10183  fin1a2lem13  10270  fpwwe2lem11  10499  suplem2pr  10911  axpre-sup  11027  axsup  11152  dedekind  11240  dedekindle  11241  fimaxre  12021  fiminre  12024  lbinf  12030  dfinfre  12058  infrelb  12062  suprfinzcl  12538  uzwo  12753  supminf  12777  lbzbi  12778  zsupss  12779  suprzcl2  12780  xrsupsslem  13143  xrinfmsslem  13144  xrub  13148  supxr2  13150  supxrun  13152  supxrunb1  13155  supxrbnd1  13157  supxrbnd2  13158  supxrub  13160  supxrbnd  13164  infxrlb  13170  elfzom1elp1fzo  13556  ssfzo12  13582  fsuppmapnn0fiublem  13812  fsuppmapnn0fiub  13813  fsuppmapnn0fiub0  13815  seqsplit  13858  shftlem  14879  rpnnen2lem10  16032  rpnnen2lem11  16033  gcdcllem1  16306  mrcuni  17428  isacs1i  17464  mreacs  17465  lubss  18329  gsumwspan  18582  subgint  18876  cntziinsn  19038  cntzsubg  19040  pmtrdifellem4  19184  subrgint  20152  cntzsubr  20163  mdetunilem9  21876  tgcl  22226  fctop  22261  cctop  22263  neips  22371  cmpsub  22658  1stcelcls  22719  ssref  22770  comppfsc  22790  txbasval  22864  fgss2  23132  filconn  23141  filuni  23143  filssufilg  23169  fmfnfmlem4  23215  trust  23488  elmopn2  23705  metrest  23787  dscopn  23836  metds0  24120  cncfmet  24179  negcncf  24192  iscmet2  24565  ovolfioo  24738  ovolficc  24739  itg1mulc  24976  ply1term  25472  plyconst  25474  reeff1olem  25712  nosupno  26958  nosupbday  26960  nosupbnd1lem5  26967  noinfno  26973  noinfbday  26975  noetasuplem4  26991  usgruspgrb  27841  ocsh  29934  ocorth  29942  spansncvi  30303  pjss1coi  30814  sumdmdii  31066  unidifsnel  31170  dfcnv2  31300  xrge0infss  31370  measdivcst  32490  measdivcstALTV  32491  dya2iocuni  32550  bnj1190  33287  nummin  33362  elxpxpss  33974  opnrebl  34648  opnrebl2  34649  fness  34677  nlpineqsn  35735  fin2so  35920  matunitlindflem1  35929  poimirlem27  35960  poimir  35966  frinfm  36049  filbcmb  36054  nnubfi  36064  nninfnub  36065  sstotbnd3  36090  bndss  36100  exidreslem  36191  isidlc  36329  idlnegcl  36336  intidl  36343  unichnidl  36345  pmapglb2N  38090  elpaddn0  38119  paddasslem9  38147  paddasslem10  38148  pclfinN  38219  polval2N  38225  diaglbN  39374  dihord6apre  39575  gneispace  42117  snsslVD  42822  snssl  42823  sstrALT2VD  42827  sstrALT2  42828  suctrALTcf  42915  suctrALTcfVD  42916  ssnel  42960  uzwo4  42973  infxrunb2  43294  infxrbnd2  43295  supxrunb3  43326  unb2ltle  43342  infxrpnf  43373  supminfxr  43391  sge0iunmptlemfi  44340  caratheodorylem2  44454  ovnlerp  44489  ssfz12  45224  prssspr  45355  prsssprel  45358  lindslinindimp2lem4  46220  lindslinindsimp2  46222  lincresunit3lem2  46239  lincresunit3  46240