Theorem sselii 3964

Description: Membership inference from subclass relationship. (Contributed by NM, 31-May-1999.)

Hypotheses

Ref	Expression
sseli.1	⊢ 𝐴 ⊆ 𝐵
sselii.2	⊢ 𝐶 ∈ 𝐴

Assertion

Ref	Expression
sselii	⊢ 𝐶 ∈ 𝐵

Proof of Theorem sselii

Step	Hyp	Ref	Expression
1		sselii.2	. 2 ⊢ 𝐶 ∈ 𝐴
2		sseli.1	. . 3 ⊢ 𝐴 ⊆ 𝐵
3	2	sseli 3963	. 2 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)
4	1, 3	ax-mp 5	1 ⊢ 𝐶 ∈ 𝐵

Syntax hints:   ∈ wcel 2110   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  sseliALT  5206  fvrn0  6693  ovima0  7321  brtpos0  7893  wfrlem16  7964  rdg0  8051  iunfi  8806  rankdmr1  9224  rankeq0b  9283  cardprclem  9402  alephfp2  9529  dfac2b  9550  sdom2en01  9718  fin56  9809  fin1a2lem10  9825  hsmexlem4  9845  canthp1lem2  10069  ax1cn  10565  recni  10649  0xr  10682  pnfxr  10689  nn0rei  11902  nn0cni  11903  0xnn0  11967  nnzi  12000  nn0zi  12001  seqexw  13379  mulgfval  18220  lbsextlem4  19927  qsubdrg  20591  leordtval2  21814  iooordt  21819  hauspwdom  22103  comppfsc  22134  dfac14  22220  filconn  22485  isufil2  22510  iooretop  23368  ovolfiniun  24096  volfiniun  24142  iblabslem  24422  iblabs  24423  bddmulibl  24433  mdegcl  24657  logcn  25224  logccv  25240  leibpi  25514  xrlimcnp  25540  jensen  25560  emre  25577  lgsdir2lem3  25897  shelii  28986  chelii  29004  omlsilem  29173  nonbooli  29422  pjssmii  29452  riesz4  29835  riesz1  29836  cnlnadjeu  29849  nmopadjlei  29859  adjeq0  29862  dp2clq  30552  rpdp2cl  30553  dp2lt10  30555  dp2lt  30556  dp2ltc  30558  dplti  30576  qqh0  31220  qqh1  31221  qqhcn  31227  rrh0  31251  esumcst  31317  esumrnmpt2  31322  volmeas  31485  hgt750lem  31917  tgoldbachgtde  31926  kur14lem7  32454  kur14lem9  32456  iinllyconn  32496  frrlem14  33131  bj-pinftyccb  34497  bj-minftyccb  34501  bj-rrdrg  34565  finixpnum  34871  poimirlem32  34918  ftc1cnnclem  34959  ftc2nc  34970  areacirclem2  34977  prdsbnd  35065  reheibor  35111  rmxyadd  39511  rmxy1  39512  rmxy0  39513  rmydioph  39604  rmxdioph  39606  expdiophlem2  39612  expdioph  39613  mpaaeu  39743  fourierdlem85  42469  fourierdlem102  42486  fourierdlem114  42498  iooborel  42627  hoicvrrex  42831