Theorem ssel2 3916

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2811  df-ss 3906

This theorem is referenced by:  tz7.7  6349  onfr  6362  onmindif  6417  ordunisssuc  6431  ssimaex  6925  nssdmovg  7549  onnmin  7752  onmindif2  7761  limsssuc  7801  el2xpss  7990  1st2nd  7992  f1o2ndf1  8072  dfrecs3  8312  boxriin  8888  ordunifi  9200  isfinite2  9208  ordtypelem7  9439  sucprcregOLD  9521  cnfcom  9621  eldju1st  9847  coflim  10183  cflim2  10185  fin23lem11  10239  fin23lem26  10247  fin1a2lem13  10334  fpwwe2lem11  10564  suplem2pr  10976  axpre-sup  11092  axsup  11221  dedekind  11309  dedekindle  11310  fimaxre  12100  fiminre  12103  lbinf  12109  dfinfre  12137  infrelb  12141  suprfinzcl  12643  uzwo  12861  supminf  12885  lbzbi  12886  zsupss  12887  suprzcl2  12888  xrsupsslem  13259  xrinfmsslem  13260  xrub  13264  supxr2  13266  supxrun  13268  supxrunb1  13271  supxrbnd1  13273  supxrbnd2  13274  supxrub  13276  supxrbnd  13280  infxrlb  13287  elfzom1elp1fzo  13687  ssfzo12  13714  fsuppmapnn0fiublem  13952  fsuppmapnn0fiub  13953  fsuppmapnn0fiub0  13955  seqsplit  13997  shftlem  15030  rpnnen2lem10  16190  rpnnen2lem11  16191  gcdcllem1  16468  mrcuni  17587  isacs1i  17623  mreacs  17624  lubss  18479  gsumwspan  18814  subgint  19126  cntziinsn  19312  cntzsubg  19314  pmtrdifellem4  19454  subrngint  20537  cntzsubrng  20544  subrgint  20572  cntzsubr  20583  sraassab  21848  mdetunilem9  22585  tgcl  22934  fctop  22969  cctop  22971  neips  23078  cmpsub  23365  1stcelcls  23426  ssref  23477  comppfsc  23497  txbasval  23571  fgss2  23839  filconn  23848  filuni  23850  filssufilg  23876  fmfnfmlem4  23922  trust  24194  elmopn2  24410  metrest  24489  dscopn  24538  metds0  24816  cncfmet  24876  negcncf  24889  iscmet2  25261  ovolfioo  25434  ovolficc  25435  itg1mulc  25671  ply1term  26169  plyconst  26171  reeff1olem  26411  nosupno  27667  nosupbday  27669  nosupbnd1lem5  27676  noinfno  27682  noinfbday  27684  noetasuplem4  27700  n0fincut  28347  usgruspgrb  29252  ocsh  31354  ocorth  31362  spansncvi  31723  pjss1coi  32234  sumdmdii  32486  unidifsnel  32605  dfcnv2  32748  xrge0infss  32833  measdivcst  34368  measdivcstALTV  34369  dya2iocuni  34427  bnj1190  35150  nummin  35236  trssfir1om  35255  trssfir1omregs  35280  opnrebl  36502  opnrebl2  36503  fness  36531  ttcmin  36678  nlpineqsn  37724  fin2so  37928  matunitlindflem1  37937  poimirlem27  37968  poimir  37974  frinfm  38056  filbcmb  38061  nnubfi  38071  nninfnub  38072  sstotbnd3  38097  bndss  38107  exidreslem  38198  isidlc  38336  idlnegcl  38343  intidl  38350  unichnidl  38352  pmapglb2N  40217  elpaddn0  40246  paddasslem9  40274  paddasslem10  40275  pclfinN  40346  polval2N  40352  diaglbN  41501  dihord6apre  41702  unielss  43646  onmaxnelsup  43651  onsupmaxb  43667  onsupeqnmax  43675  gneispace  44561  snsslVD  45255  snssl  45256  sstrALT2VD  45260  sstrALT2  45261  suctrALTcf  45348  suctrALTcfVD  45349  ssnel  45474  uzwo4  45484  infxrunb2  45797  infxrbnd2  45798  supxrunb3  45828  unb2ltle  45843  infxrpnf  45874  supminfxr  45892  sge0iunmptlemfi  46841  caratheodorylem2  46955  ovnlerp  46990  ssfz12  47762  prssspr  47945  prsssprel  47948  lindslinindimp2lem4  48937  lindslinindsimp2  48939  lincresunit3lem2  48956  lincresunit3  48957