Theorem ssel2 3933

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

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

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 2148

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

This theorem is used by:  tz7.7  6390  onfr  6404  onmindif  6459  ordunisssuc  6473  ssimaex  6970  nssdmovg  7598  onnmin  7799  onmindif2  7808  limsssuc  7848  el2xpss  8036  1st2nd  8038  f1o2ndf1  8119  dfrecs3  8361  boxriin  8940  ordunifi  9253  isfinite2  9261  ordtypelem7  9489  sucprcregOLD  9572  cnfcom  9672  eldju1st  9921  coflim  10256  cflim2  10258  fin23lem11  10312  fin23lem26  10320  fin1a2lem13  10407  fpwwe2lem11  10637  suplem2pr  11049  axpre-sup  11165  axsup  11296  dedekind  11384  dedekindle  11385  fimaxre  12170  fiminre  12173  lbinf  12179  dfinfre  12207  infrelb  12211  suprfinzcl  12721  uzwo  12946  supminf  12970  lbzbi  12971  zsupss  12972  suprzcl2  12973  xrsupsslem  13344  xrinfmsslem  13345  xrub  13349  supxr2  13351  supxrun  13353  supxrunb1  13356  supxrbnd1  13358  supxrbnd2  13359  supxrub  13361  supxrbnd  13365  infxrlb  13372  elfzom1elp1fzo  13773  ssfzo12  13800  fsuppmapnn0fiublem  14039  fsuppmapnn0fiub  14040  fsuppmapnn0fiub0  14042  seqsplit  14084  shftlem  15124  rpnnen2lem10  16296  rpnnen2lem11  16297  gcdcllem1  16574  mrcuni  17694  isacs1i  17730  mreacs  17731  lubss  18586  gsumwspan  18928  subgint  19240  cntziinsn  19430  cntzsubg  19432  pmtrdifellem4  19572  subrngint  20688  cntzsubrng  20695  subrgint  20723  cntzsubr  20734  sraassab  22047  mdetunilem9  22806  tgcl  23155  fctop  23190  cctop  23192  neips  23299  cmpsub  23586  1stcelcls  23647  ssref  23698  comppfsc  23718  txbasval  23792  fgss2  24060  filconn  24069  filuni  24071  filssufilg  24097  fmfnfmlem4  24143  trust  24415  elmopn2  24631  metrest  24710  dscopn  24759  metds0  25037  cncfmet  25097  negcncf  25110  iscmet2  25482  ovolfioo  25655  ovolficc  25656  itg1mulc  25892  ply1term  26390  plyconst  26392  reeff1olem  26638  nosupno  27896  nosupbday  27898  nosupbnd1lem5  27905  noinfno  27911  noinfbday  27913  noetasuplem4  27929  n0fincut  28577  usgruspgrb  29562  ocsh  31664  ocorth  31672  spansncvi  32033  pjss1coi  32544  sumdmdii  32796  unidifsnel  32910  dfcnv2  33049  xrge0infss  33134  measdivcst  34638  measdivcstALTV  34639  dya2iocuni  34697  bnj1190  35420  nummin  35501  trssfir1om  35524  trssfir1omregs  35565  opnrebl  36864  opnrebl2  36865  fness  36893  ttcmin  37040  nlpineqsn  38087  fin2so  38291  matunitlindflem1  38300  poimirlem27  38331  poimir  38337  frinfm  38419  filbcmb  38424  nnubfi  38434  nninfnub  38435  sstotbnd3  38460  bndss  38470  exidreslem  38561  isidlc  38699  idlnegcl  38706  intidl  38713  unichnidl  38715  pmapglb2N  40578  elpaddn0  40607  paddasslem9  40635  paddasslem10  40636  pclfinN  40707  polval2N  40713  diaglbN  41862  dihord6apre  42063  unielss  43978  onmaxnelsup  43983  onsupmaxb  43999  onsupeqnmax  44007  gneispace  44893  snsslVD  45570  snssl  45571  sstrALT2VD  45575  sstrALT2  45576  suctrALTcf  45663  suctrALTcfVD  45664  ssnel  45796  uzwo4  45806  infxrunb2  46116  infxrbnd2  46117  supxrunb3  46147  unb2ltle  46162  infxrpnf  46193  supminfxr  46211  sge0iunmptlemfi  47160  caratheodorylem2  47274  ovnlerp  47309  ssfz12  48084  prssspr  48267  prsssprel  48270  lindslinindimp2lem4  49274  lindslinindsimp2  49276  lincresunit3lem2  49293  lincresunit3  49294