Theorem sselii 3934

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

Syntax hints:   ∈ wcel 2143   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-clel 2838  df-ss 3922

This theorem is referenced by:  sseliALT  5272  fvrn0  6909  ovima0  7589  brtpos0  8225  frrlem14  8292  rdg0  8404  iunfi  9296  rankdmr1  9769  rankeq0b  9828  cardprclem  9961  alephfp2  10089  dfac2b  10110  sdom2en01  10281  fin56  10372  fin1a2lem10  10388  hsmexlem4  10408  canthp1lem2  10633  ax1cn  11129  recni  11218  0xr  11251  pnfxr  11258  nn0rei  12510  nn0cni  12511  0xnn0  12578  nnzi  12613  nn0zi  12614  seqexw  14049  mulgfval  19130  lbsextlem4  21285  qsubdrg  21569  leordtval2  23369  iooordt  23374  hauspwdom  23658  comppfsc  23689  dfac14  23775  filconn  24040  isufil2  24065  iooretop  24922  ovolfiniun  25660  volfiniun  25706  iblabslem  25987  iblabs  25988  bddmulibl  25998  mdegcl  26226  0aa  26486  1aa  26487  logcn  26812  logccv  26828  leibpi  27107  xrlimcnp  27133  jensen  27153  emre  27170  lgsdir2lem3  27491  shelii  31567  chelii  31585  omlsilem  31754  nonbooli  32003  pjssmii  32033  riesz4  32416  riesz1  32417  cnlnadjeu  32430  nmopadjlei  32440  adjeq0  32443  dp2clq  33200  rpdp2cl  33201  dp2lt10  33203  dp2lt  33204  dp2ltc  33206  dplti  33224  zringfrac  33844  vieta  33970  qqh0  34374  qqh1  34375  qqhcn  34381  rrh0  34405  esumcst  34453  esumrnmpt2  34458  volmeas  34621  hgt750lem  35038  tgoldbachgtde  35047  kur14lem7  35704  kur14lem9  35706  iinllyconn  35746  bj-rdg0gALT  37707  bj-pinftyccb  37865  bj-minftyccb  37869  bj-rrdrg  37934  finixpnum  38256  poimirlem32  38303  ftc1cnnclem  38342  ftc2nc  38353  areacirclem2  38360  prdsbnd  38444  reheibor  38490  rmxyadd  43648  rmxy1  43649  rmxy0  43650  rmydioph  43741  rmxdioph  43743  expdiophlem2  43749  expdioph  43750  mpaaeu  43877  0iscard  44267  1iscard  44268  wfaxrep  45703  wfaxnul  45705  wfaxinf2  45710  fourierdlem85  46905  fourierdlem102  46922  fourierdlem114  46934  iooborel  47065  hoicvrrex  47270  lamberte  47625