Theorem ssel2 3926

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2836  df-ss 3916

This theorem is used by:  tz7.7  6387  onfr  6401  onmindif  6456  ordunisssuc  6470  ssimaex  6968  nssdmovg  7601  onnmin  7810  onmindif2  7819  limsssuc  7859  el2xpss  8046  1st2nd  8048  f1o2ndf1  8131  dfrecs3  8373  onelfvnef1  8442  boxriin  8961  ordunifi  9274  isfinite2  9283  ordtypelem7  9511  sucprcregOLD  9594  cnfcom  9694  elhf3OLD  9916  eldju1st  9997  coflim  10332  cflim2  10334  fin23lem11  10388  fin23lem26  10396  fin1a2lem13  10483  fpwwe2lem11  10719  suplem2pr  11131  axpre-sup  11247  axsup  11378  dedekind  11466  dedekindle  11467  fimaxre  12254  fiminre  12257  lbinf  12263  dfinfre  12291  infrelb  12295  suprfinzcl  12806  uzwo  13031  supminf  13055  lbzbi  13056  zsupss  13057  suprzcl2  13058  xrsupsslem  13430  xrinfmsslem  13431  xrub  13435  supxr2  13437  supxrun  13439  supxrunb1  13442  supxrbnd1  13444  supxrbnd2  13445  supxrub  13447  supxrbnd  13451  infxrlb  13458  elfzom1elp1fzo  13860  ssfzo12  13887  fsuppmapnn0fiublem  14126  fsuppmapnn0fiub  14127  fsuppmapnn0fiub0  14129  seqsplit  14171  shftlem  15214  rpnnen2lem10  16384  rpnnen2lem11  16385  gcdcllem1  16662  mrcuni  17788  isacs1i  17824  mreacs  17825  lubss  18680  gsumwspan  19035  subgint  19354  cntziinsn  19544  cntzsubg  19546  pmtrdifellem4  19686  subrngint  20805  cntzsubrng  20812  subrgint  20840  cntzsubr  20851  sraassab  22169  mdetunilem9  22928  matunitlindflem1  22987  tgcl  23280  fctop  23315  cctop  23317  neips  23424  cmpsub  23711  1stcelcls  23773  ssref  23824  comppfsc  23844  txbasval  23918  fgss2  24186  filconn  24195  filuni  24197  filssufilg  24223  fmfnfmlem4  24269  trust  24541  elmopn2  24757  metrest  24836  dscopn  24885  metds0  25163  cncfmet  25223  negcncf  25236  iscmet2  25608  ovolfioo  25781  ovolficc  25782  itg1mulc  26018  ply1term  26515  plyconst  26517  reeff1olem  26766  nosupno  28053  nosupbday  28055  nosupbnd1lem5  28062  noinfno  28068  noinfbday  28070  noetasuplem4  28086  n0fincut  28734  usgruspgrb  29757  ocsh  31878  ocorth  31886  spansncvi  32247  pjss1coi  32758  sumdmdii  33010  unidifsnel  33124  dfcnv2  33262  xrge0infss  33345  measdivcst  34850  measdivcstALTV  34851  dya2iocuni  34908  bnj1190  35631  nummin  35711  trssfir1om  35726  trssfir1omregs  35787  opnrebl  37088  opnrebl2  37089  fness  37117  ttcmin  37264  nlpineqsn  38311  fin2so  38510  poimirlem27  38545  poimir  38551  frinfm  38649  filbcmb  38654  nnubfi  38664  nninfnub  38665  sstotbnd3  38690  bndss  38700  exidreslem  38791  isidlc  38929  idlnegcl  38936  intidl  38943  unichnidl  38945  pmapglb2N  40808  elpaddn0  40837  paddasslem9  40865  paddasslem10  40866  pclfinN  40937  polval2N  40943  diaglbN  42092  dihord6apre  42293  unielss  44204  onmaxnelsup  44209  onsupmaxb  44225  onsupeqnmax  44233  gneispace  45119  snsslVD  45796  snssl  45797  sstrALT2VD  45801  sstrALT2  45802  suctrALTcf  45889  suctrALTcfVD  45890  ssnel  46029  uzwo4  46039  infxrunb2  46348  infxrbnd2  46349  supxrunb3  46379  unb2ltle  46394  infxrpnf  46425  supminfxr  46443  sge0iunmptlemfi  47392  caratheodorylem2  47506  ovnlerp  47541  ssfz12  48353  prssspr  48536  prsssprel  48539  lindslinindimp2lem4  49542  lindslinindsimp2  49544  lincresunit3lem2  49561  lincresunit3  49562