Theorem sselii 3931

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

Syntax hints:   ∈ wcel 2141   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-clel 2836  df-ss 3919

This theorem is referenced by:  sseliALT  5256  fvrn0  6890  ovima0  7570  brtpos0  8207  frrlem14  8274  rdg0  8386  iunfi  9280  rankdmr1  9753  rankeq0b  9812  cardprclem  9931  alephfp2  10059  dfac2b  10081  sdom2en01  10253  fin56  10344  fin1a2lem10  10360  hsmexlem4  10380  canthp1lem2  10605  ax1cn  11101  recni  11190  0xr  11223  pnfxr  11230  nn0rei  12486  nn0cni  12487  0xnn0  12554  nnzi  12589  nn0zi  12590  seqexw  14024  mulgfval  19102  lbsextlem4  21219  qsubdrg  21459  leordtval2  23260  iooordt  23265  hauspwdom  23549  comppfsc  23580  dfac14  23666  filconn  23931  isufil2  23956  iooretop  24813  ovolfiniun  25551  volfiniun  25597  iblabslem  25878  iblabs  25879  bddmulibl  25889  mdegcl  26117  logcn  26700  logccv  26716  leibpi  26995  xrlimcnp  27021  jensen  27041  emre  27058  lgsdir2lem3  27379  shelii  31375  chelii  31393  omlsilem  31562  nonbooli  31811  pjssmii  31841  riesz4  32224  riesz1  32225  cnlnadjeu  32238  nmopadjlei  32248  adjeq0  32251  dp2clq  33019  rpdp2cl  33020  dp2lt10  33022  dp2lt  33023  dp2ltc  33025  dplti  33043  zringfrac  33711  vieta  33838  qqh0  34242  qqh1  34243  qqhcn  34249  rrh0  34273  esumcst  34321  esumrnmpt2  34326  volmeas  34489  hgt750lem  34906  tgoldbachgtde  34915  kur14lem7  35523  kur14lem9  35525  iinllyconn  35565  bj-rdg0gALT  37517  bj-pinftyccb  37674  bj-minftyccb  37678  bj-rrdrg  37743  finixpnum  38065  poimirlem32  38112  ftc1cnnclem  38151  ftc2nc  38162  areacirclem2  38169  prdsbnd  38253  reheibor  38299  rmxyadd  43459  rmxy1  43460  rmxy0  43461  rmydioph  43552  rmxdioph  43554  expdiophlem2  43560  expdioph  43561  mpaaeu  43688  0iscard  44078  1iscard  44079  wfaxrep  45531  wfaxnul  45533  wfaxinf2  45538  fourierdlem85  46726  fourierdlem102  46743  fourierdlem114  46755  iooborel  46886  hoicvrrex  47091  lamberte  47443