Theorem sselii 3758

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

Syntax hints:   ∈ wcel 2155   ⊆ wss 3732

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-in 3739  df-ss 3746

This theorem is referenced by:  sseliALT  4952  fvrn0  6403  ovima0  7011  brtpos0  7562  wfrlem16  7634  rdg0  7721  iunfi  8461  rankdmr1  8879  rankeq0b  8938  cardprclem  9056  alephfp2  9183  dfac2b  9204  dfac2OLD  9206  sdom2en01  9377  fin56  9468  fin1a2lem10  9484  hsmexlem4  9504  canthp1lem2  9728  ax1cn  10223  recni  10308  0xr  10340  pnfxr  10346  nn0rei  11550  nn0cni  11551  0xnn0  11616  nnzi  11648  nn0zi  11649  fprodge0  15008  lbsextlem4  19435  qsubdrg  20071  leordtval2  21296  iooordt  21301  hauspwdom  21584  comppfsc  21615  dfac14  21701  filconn  21966  isufil2  21991  iooretop  22848  ovolfiniun  23559  volfiniun  23605  iblabslem  23885  iblabs  23886  bddmulibl  23896  mdegcl  24120  logcn  24684  logccv  24700  leibpi  24960  xrlimcnp  24986  jensen  25006  emre  25023  lgsdir2lem3  25343  tgcgr4  25717  shelii  28463  chelii  28481  omlsilem  28652  nonbooli  28901  pjssmii  28931  riesz4  29314  riesz1  29315  cnlnadjeu  29328  nmopadjlei  29338  adjeq0  29341  dp2clq  29971  rpdp2cl  29972  dp2lt10  29974  dp2lt  29975  dp2ltc  29977  dplti  29995  qqh0  30410  qqh1  30411  qqhcn  30417  rrh0  30441  esumcst  30507  esumrnmpt2  30512  volmeas  30676  hgt750lem  31112  tgoldbachgtde  31121  kur14lem7  31574  kur14lem9  31576  iinllyconn  31616  bj-pinftyccb  33474  bj-minftyccb  33478  finixpnum  33750  poimirlem32  33797  ftc1cnnclem  33838  ftc2nc  33849  areacirclem2  33856  prdsbnd  33946  reheibor  33992  rmxyadd  38095  rmxy1  38096  rmxy0  38097  rmydioph  38190  rmxdioph  38192  expdiophlem2  38198  expdioph  38199  mpaaeu  38329  fourierdlem85  40977  fourierdlem102  40994  fourierdlem114  41006  iooborel  41138  hoicvrrex  41342