Theorem sselii 3932

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 3931	. 2 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)
4	1, 3	ax-mp 5	1 ⊢ 𝐶 ∈ 𝐵

Syntax hints:   ∈ wcel 2114   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812  df-ss 3920

This theorem is referenced by:  sseliALT  5256  fvrn0  6870  ovima0  7547  brtpos0  8185  frrlem14  8251  rdg0  8362  iunfi  9255  rankdmr1  9725  rankeq0b  9784  cardprclem  9903  alephfp2  10031  dfac2b  10053  sdom2en01  10224  fin56  10315  fin1a2lem10  10331  hsmexlem4  10351  canthp1lem2  10576  ax1cn  11072  recni  11158  0xr  11191  pnfxr  11198  nn0rei  12424  nn0cni  12425  0xnn0  12492  nnzi  12527  nn0zi  12528  seqexw  13952  mulgfval  19011  lbsextlem4  21128  qsubdrg  21386  leordtval2  23168  iooordt  23173  hauspwdom  23457  comppfsc  23488  dfac14  23574  filconn  23839  isufil2  23864  iooretop  24721  ovolfiniun  25470  volfiniun  25516  iblabslem  25797  iblabs  25798  bddmulibl  25808  mdegcl  26042  logcn  26624  logccv  26640  leibpi  26920  xrlimcnp  26946  jensen  26967  emre  26984  lgsdir2lem3  27306  shelii  31303  chelii  31321  omlsilem  31490  nonbooli  31739  pjssmii  31769  riesz4  32152  riesz1  32153  cnlnadjeu  32166  nmopadjlei  32176  adjeq0  32179  dp2clq  32973  rpdp2cl  32974  dp2lt10  32976  dp2lt  32977  dp2ltc  32979  dplti  32997  zringfrac  33647  vieta  33757  qqh0  34162  qqh1  34163  qqhcn  34169  rrh0  34193  esumcst  34241  esumrnmpt2  34246  volmeas  34409  hgt750lem  34829  tgoldbachgtde  34838  kur14lem7  35428  kur14lem9  35430  iinllyconn  35470  exeltr  36687  bj-rdg0gALT  37319  bj-pinftyccb  37476  bj-minftyccb  37480  bj-rrdrg  37545  finixpnum  37856  poimirlem32  37903  ftc1cnnclem  37942  ftc2nc  37953  areacirclem2  37960  prdsbnd  38044  reheibor  38090  rmxyadd  43278  rmxy1  43279  rmxy0  43280  rmydioph  43371  rmxdioph  43373  expdiophlem2  43379  expdioph  43380  mpaaeu  43507  0iscard  43897  1iscard  43898  wfaxrep  45350  wfaxnul  45352  wfaxinf2  45357  fourierdlem85  46549  fourierdlem102  46566  fourierdlem114  46578  iooborel  46709  hoicvrrex  46914  lamberte  47248