Theorem sselii 3944

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

Syntax hints:   ∈ wcel 2106   ⊆ wss 3913

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  sseliALT  5271  fvrn0  6877  ovima0  7538  brtpos0  8169  frrlem14  8235  wfrlem16OLD  8275  rdg0  8372  iunfi  9291  rankdmr1  9746  rankeq0b  9805  cardprclem  9924  alephfp2  10054  dfac2b  10075  sdom2en01  10247  fin56  10338  fin1a2lem10  10354  hsmexlem4  10374  canthp1lem2  10598  ax1cn  11094  recni  11178  0xr  11211  pnfxr  11218  nn0rei  12433  nn0cni  12434  0xnn0  12500  nnzi  12536  nn0zi  12537  seqexw  13932  mulgfval  18888  lbsextlem4  20681  qsubdrg  20886  leordtval2  22600  iooordt  22605  hauspwdom  22889  comppfsc  22920  dfac14  23006  filconn  23271  isufil2  23296  iooretop  24166  ovolfiniun  24902  volfiniun  24948  iblabslem  25229  iblabs  25230  bddmulibl  25240  mdegcl  25471  logcn  26039  logccv  26055  leibpi  26329  xrlimcnp  26355  jensen  26375  emre  26392  lgsdir2lem3  26712  shelii  30220  chelii  30238  omlsilem  30407  nonbooli  30656  pjssmii  30686  riesz4  31069  riesz1  31070  cnlnadjeu  31083  nmopadjlei  31093  adjeq0  31096  dp2clq  31807  rpdp2cl  31808  dp2lt10  31810  dp2lt  31811  dp2ltc  31813  dplti  31831  qqh0  32654  qqh1  32655  qqhcn  32661  rrh0  32685  esumcst  32751  esumrnmpt2  32756  volmeas  32919  hgt750lem  33353  tgoldbachgtde  33362  kur14lem7  33893  kur14lem9  33895  iinllyconn  33935  bj-rdg0gALT  35615  bj-pinftyccb  35765  bj-minftyccb  35769  bj-rrdrg  35834  finixpnum  36136  poimirlem32  36183  ftc1cnnclem  36222  ftc2nc  36233  areacirclem2  36240  prdsbnd  36325  reheibor  36371  rmxyadd  41303  rmxy1  41304  rmxy0  41305  rmydioph  41396  rmxdioph  41398  expdiophlem2  41404  expdioph  41405  mpaaeu  41535  0iscard  41935  1iscard  41936  fourierdlem85  44552  fourierdlem102  44569  fourierdlem114  44581  iooborel  44712  hoicvrrex  44917