Theorem ssel2 3977

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3955  df-ss 3965

This theorem is referenced by:  tz7.7  6388  onfr  6401  onmindif  6454  ordunisssuc  6468  ssimaex  6974  nssdmovg  7586  onnmin  7783  onmindif2  7792  limsssuc  7836  el2xpss  8020  1st2nd  8022  f1o2ndf1  8105  dfrecs3  8369  dfrecs3OLD  8370  boxriin  8931  ordunifi  9290  isfinite2  9298  ordtypelem7  9516  sucprcreg  9593  cnfcom  9692  eldju1st  9915  coflim  10253  cflim2  10255  fin23lem11  10309  fin23lem26  10317  fin1a2lem13  10404  fpwwe2lem11  10633  suplem2pr  11045  axpre-sup  11161  axsup  11286  dedekind  11374  dedekindle  11375  fimaxre  12155  fiminre  12158  lbinf  12164  dfinfre  12192  infrelb  12196  suprfinzcl  12673  uzwo  12892  supminf  12916  lbzbi  12917  zsupss  12918  suprzcl2  12919  xrsupsslem  13283  xrinfmsslem  13284  xrub  13288  supxr2  13290  supxrun  13292  supxrunb1  13295  supxrbnd1  13297  supxrbnd2  13298  supxrub  13300  supxrbnd  13304  infxrlb  13310  elfzom1elp1fzo  13696  ssfzo12  13722  fsuppmapnn0fiublem  13952  fsuppmapnn0fiub  13953  fsuppmapnn0fiub0  13955  seqsplit  13998  shftlem  15012  rpnnen2lem10  16163  rpnnen2lem11  16164  gcdcllem1  16437  mrcuni  17562  isacs1i  17598  mreacs  17599  lubss  18463  gsumwspan  18724  subgint  19025  cntziinsn  19196  cntzsubg  19198  pmtrdifellem4  19342  subrgint  20379  cntzsubr  20391  sraassab  21414  mdetunilem9  22114  tgcl  22464  fctop  22499  cctop  22501  neips  22609  cmpsub  22896  1stcelcls  22957  ssref  23008  comppfsc  23028  txbasval  23102  fgss2  23370  filconn  23379  filuni  23381  filssufilg  23407  fmfnfmlem4  23453  trust  23726  elmopn2  23943  metrest  24025  dscopn  24074  metds0  24358  cncfmet  24417  negcncf  24430  iscmet2  24803  ovolfioo  24976  ovolficc  24977  itg1mulc  25214  ply1term  25710  plyconst  25712  reeff1olem  25950  nosupno  27196  nosupbday  27198  nosupbnd1lem5  27205  noinfno  27211  noinfbday  27213  noetasuplem4  27229  usgruspgrb  28431  ocsh  30524  ocorth  30532  spansncvi  30893  pjss1coi  31404  sumdmdii  31656  unidifsnel  31760  dfcnv2  31889  xrge0infss  31961  measdivcst  33211  measdivcstALTV  33212  dya2iocuni  33271  bnj1190  34008  nummin  34083  gg-negcncf  35155  opnrebl  35194  opnrebl2  35195  fness  35223  nlpineqsn  36278  fin2so  36464  matunitlindflem1  36473  poimirlem27  36504  poimir  36510  frinfm  36592  filbcmb  36597  nnubfi  36607  nninfnub  36608  sstotbnd3  36633  bndss  36643  exidreslem  36734  isidlc  36872  idlnegcl  36879  intidl  36886  unichnidl  36888  pmapglb2N  38631  elpaddn0  38660  paddasslem9  38688  paddasslem10  38689  pclfinN  38760  polval2N  38766  diaglbN  39915  dihord6apre  40116  unielss  41953  onmaxnelsup  41958  onsupmaxb  41974  onsupeqnmax  41982  gneispace  42871  snsslVD  43576  snssl  43577  sstrALT2VD  43581  sstrALT2  43582  suctrALTcf  43669  suctrALTcfVD  43670  ssnel  43713  uzwo4  43726  infxrunb2  44065  infxrbnd2  44066  supxrunb3  44096  unb2ltle  44112  infxrpnf  44143  supminfxr  44161  sge0iunmptlemfi  45116  caratheodorylem2  45230  ovnlerp  45265  ssfz12  46009  prssspr  46140  prsssprel  46143  subrngint  46724  cntzsubrng  46731  lindslinindimp2lem4  47096  lindslinindsimp2  47098  lincresunit3lem2  47115  lincresunit3  47116