Theorem ssel2 3903

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-clel 2835  df-ss 3896

This theorem is used by:  tz7.7  6388  onfr  6402  onmindif  6457  ordunisssuc  6471  ssimaex  6971  nssdmovg  7604  onnmin  7813  onmindif2  7822  limsssuc  7862  el2xpss  8049  1st2nd  8051  f1o2ndf1  8136  dfrecs3  8384  onelfvnef1  8453  boxriin  8972  ordunifi  9285  isfinite2  9294  ordtypelem7  9522  sucprcregOLD  9605  cnfcom  9705  elhf3OLD  9927  eldju1st  10008  coflim  10343  cflim2  10345  fin23lem11  10399  fin23lem26  10407  fin1a2lem13  10494  fpwwe2lem11  10730  suplem2pr  11142  axpre-sup  11258  axsup  11389  dedekind  11477  dedekindle  11478  fimaxre  12265  fiminre  12268  lbinf  12274  dfinfre  12302  infrelb  12306  suprfinzcl  12817  uzwo  13042  supminf  13066  lbzbi  13067  zsupss  13068  suprzcl2  13069  xrsupsslem  13441  xrinfmsslem  13442  xrub  13446  supxr2  13448  supxrun  13450  supxrunb1  13453  supxrbnd1  13455  supxrbnd2  13456  supxrub  13458  supxrbnd  13462  infxrlb  13469  elfzom1elp1fzo  13871  ssfzo12  13898  fsuppmapnn0fiublem  14137  fsuppmapnn0fiub  14138  fsuppmapnn0fiub0  14140  seqsplit  14182  shftlem  15227  rpnnen2lem10  16397  rpnnen2lem11  16398  gcdcllem1  16675  mrcuni  17801  isacs1i  17837  mreacs  17838  lubss  18693  gsumwspan  19048  subgint  19367  cntziinsn  19557  cntzsubg  19559  pmtrdifellem4  19699  subrngint  20818  cntzsubrng  20825  subrgint  20853  cntzsubr  20864  sraassab  22182  mdetunilem9  22941  matunitlindflem1  23000  tgcl  23293  fctop  23328  cctop  23330  neips  23437  cmpsub  23724  1stcelcls  23786  ssref  23837  comppfsc  23857  txbasval  23931  fgss2  24199  filconn  24208  filuni  24210  filssufilg  24236  fmfnfmlem4  24282  trust  24554  elmopn2  24770  metrest  24849  dscopn  24898  metds0  25176  cncfmet  25236  negcncf  25249  iscmet2  25621  ovolfioo  25794  ovolficc  25795  itg1mulc  26031  ply1term  26528  plyconst  26530  reeff1olem  26779  nosupno  28066  nosupbday  28068  nosupbnd1lem5  28075  noinfno  28081  noinfbday  28083  noetasuplem4  28099  n0fincut  28747  usgruspgrb  29770  ocsh  31891  ocorth  31899  spansncvi  32260  pjss1coi  32771  sumdmdii  33023  unidifsnel  33179  dfcnv2  33317  xrge0infss  33399  measdivcst  34904  measdivcstALTV  34905  dya2iocuni  34962  bnj1190  35685  nummin  35775  trssfir1om  35790  trssfir1omregs  35861  onprcf1acwevdlem1  35965  opnrebl  37201  opnrebl2  37202  fness  37230  ttcmin  37377  nlpineqsn  38425  fin2so  38624  poimirlem27  38659  poimir  38665  frinfm  38763  filbcmb  38768  nnubfi  38778  nninfnub  38779  sstotbnd3  38804  bndss  38814  exidreslem  38905  isidlc  39043  idlnegcl  39050  intidl  39057  unichnidl  39059  pmapglb2N  40922  elpaddn0  40951  paddasslem9  40979  paddasslem10  40980  pclfinN  41051  polval2N  41057  diaglbN  42206  dihord6apre  42407  unielss  44314  onmaxnelsup  44319  onsupmaxb  44335  onsupeqnmax  44343  gneispace  45228  snsslVD  45905  snssl  45906  sstrALT2VD  45910  sstrALT2  45911  suctrALTcf  45998  suctrALTcfVD  45999  ssnel  46154  uzwo4  46164  infxrunb2  46473  infxrbnd2  46474  supxrunb3  46504  unb2ltle  46519  infxrpnf  46550  supminfxr  46568  sge0iunmptlemfi  47517  caratheodorylem2  47631  ovnlerp  47666  ssfz12  48478  prssspr  48661  prsssprel  48664  lindslinindimp2lem4  49667  lindslinindsimp2  49669  lincresunit3lem2  49686  lincresunit3  49687