Theorem sselii 3912

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

Syntax hints:   ∈ wcel 2119   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-clel 2814  df-ss 3900

This theorem is referenced by:  sseliALT  5231  fvrn0  6855  ovima0  7535  brtpos0  8173  frrlem14  8239  rdg0  8350  iunfi  9243  rankdmr1  9716  rankeq0b  9775  cardprclem  9894  alephfp2  10022  dfac2b  10044  sdom2en01  10215  fin56  10306  fin1a2lem10  10322  hsmexlem4  10342  canthp1lem2  10567  ax1cn  11063  recni  11150  0xr  11183  pnfxr  11190  nn0rei  12439  nn0cni  12440  0xnn0  12507  nnzi  12542  nn0zi  12543  seqexw  13970  mulgfval  19036  lbsextlem4  21154  qsubdrg  21394  leordtval2  23195  iooordt  23200  hauspwdom  23484  comppfsc  23515  dfac14  23601  filconn  23866  isufil2  23891  iooretop  24748  ovolfiniun  25486  volfiniun  25532  iblabslem  25813  iblabs  25814  bddmulibl  25824  mdegcl  26052  logcn  26629  logccv  26645  leibpi  26924  xrlimcnp  26950  jensen  26970  emre  26987  lgsdir2lem3  27308  shelii  31304  chelii  31322  omlsilem  31491  nonbooli  31740  pjssmii  31770  riesz4  32153  riesz1  32154  cnlnadjeu  32167  nmopadjlei  32177  adjeq0  32180  dp2clq  32959  rpdp2cl  32960  dp2lt10  32962  dp2lt  32963  dp2ltc  32965  dplti  32983  zringfrac  33637  vieta  33764  qqh0  34168  qqh1  34169  qqhcn  34175  rrh0  34199  esumcst  34247  esumrnmpt2  34252  volmeas  34415  hgt750lem  34835  tgoldbachgtde  34844  kur14lem7  35440  kur14lem9  35442  iinllyconn  35482  bj-rdg0gALT  37424  bj-pinftyccb  37581  bj-minftyccb  37585  bj-rrdrg  37650  finixpnum  37972  poimirlem32  38019  ftc1cnnclem  38058  ftc2nc  38069  areacirclem2  38076  prdsbnd  38160  reheibor  38206  rmxyadd  43366  rmxy1  43367  rmxy0  43368  rmydioph  43459  rmxdioph  43461  expdiophlem2  43467  expdioph  43468  mpaaeu  43595  0iscard  43985  1iscard  43986  wfaxrep  45438  wfaxnul  45440  wfaxinf2  45445  fourierdlem85  46634  fourierdlem102  46651  fourierdlem114  46663  iooborel  46794  hoicvrrex  46999  lamberte  47351