Theorem ssel2 2116

Description: Membership relationships follow from a subclass relationship.

Assertion

Ref	Expression
ssel2	⊢ ((A ⊆ B ⋀ C ∈ A) → C ∈ B)

Proof of Theorem ssel2

Step	Hyp	Ref	Expression
1		ssel 2115	. 2 ⊢ (A ⊆ B → (C ∈ A → C ∈ B))
2	1	imp 348	1 ⊢ ((A ⊆ B ⋀ C ∈ A) → C ∈ B)

Syntax hints:   → wi 3   ⋀ wa 221   ∈ wcel 994   ⊆ wss 2099

This theorem is referenced by:  tz7.7 3001  onmindif 3061  ordunisssuc 3072  onnmin 3160  onmindif2 3169  limsssuc 3204  ssimaex 3879  1st2nd 4168  fundmen 4569  isfinite2 4692  suplem2pr 5316  axsup 5661  lbinfm 6216  suprleub 6227  dfinfmr 6235  infmrcl 6237  xrsupsslem 6244  xrinfmsslem 6245  xrub 6248  supxr2 6250  supxrre 6251  supxrun 6253  supxrunb1 6257  supxrbnd 6259  supxrbnd1 6263  supxrbnd2 6264  supxrub 6266  supxrleub 6267  uzwo4OLD 6381  uzwo 6582  uzwoOLD 6583  shftf 6716  sumeqfv 7200  infxpidmlem5 7768  infxpidmlem7 7770  infxpidmlem8 7771  tgcl 7836  cctop 7862  neips 7937  isopn4 8072  opni3 8076  opnuni 8078  lpbl 8090  metequiv 8091  metcnplem 8097  metelcls 8176  ubthlem11 8797  ocsh 9432  ocorth 9440  spansncvi 9875  pjss1coi 10371  sumdmdii 10624  tostos 10883  efilcp 11083  efilcp2 11087  xpss1 11403  xpss2 11404  fiuni 11420  compsublem 11487  compsub 11488  hscptsscld 11491  compfipin0lem 11492  compfipin0 11493  cncomp 11494  subtopmetlem 11505  subtopmet 11506  reconnlem1 11507  reconn 11512  isfne3 11543  fness 11552  ssref 11553  comppfsc 11578  neibastop2lem3 11582  topjoin 11588  fnemeet1 11589  fnemeet2 11590  fnejoin1 11591  fgbas 11636  fbfgss 11640  limfilcf 11683  fmfnfmlem4 11703  fcluscomp 11733  ssga 11777  fipreima 11848  frinfm 11850  filbcmb 11857  nnubfi 11881  nninfnub 11882  blssp 11908  metsstop 11909  mettrifi 11912  mettrifi2 11913  geomcau 11914  lmtlm 11969  uptx 11978  txsubsp 11983  sstotbnd 11992  totbndss 11993  bndss 11998  totbndbnd 12000  heiborlem8 12018  heiborlem10 12020  heiborlem11 12021  heiborlem13 12023  rrntotbnd 12078

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-in 2103  df-ss 2105

Copyright terms: Public domain