Theorem sselii 4005

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

Syntax hints:   ∈ wcel 2108   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-clel 2819  df-ss 3993

This theorem is referenced by:  sseliALT  5327  fvrn0  6950  ovima0  7629  brtpos0  8274  frrlem14  8340  wfrlem16OLD  8380  rdg0  8477  iunfi  9411  rankdmr1  9870  rankeq0b  9929  cardprclem  10048  alephfp2  10178  dfac2b  10200  sdom2en01  10371  fin56  10462  fin1a2lem10  10478  hsmexlem4  10498  canthp1lem2  10722  ax1cn  11218  recni  11304  0xr  11337  pnfxr  11344  nn0rei  12564  nn0cni  12565  0xnn0  12631  nnzi  12667  nn0zi  12668  seqexw  14068  mulgfval  19109  lbsextlem4  21186  qsubdrg  21460  leordtval2  23241  iooordt  23246  hauspwdom  23530  comppfsc  23561  dfac14  23647  filconn  23912  isufil2  23937  iooretop  24807  ovolfiniun  25555  volfiniun  25601  iblabslem  25883  iblabs  25884  bddmulibl  25894  mdegcl  26128  logcn  26707  logccv  26723  leibpi  27003  xrlimcnp  27029  jensen  27050  emre  27067  lgsdir2lem3  27389  shelii  31247  chelii  31265  omlsilem  31434  nonbooli  31683  pjssmii  31713  riesz4  32096  riesz1  32097  cnlnadjeu  32110  nmopadjlei  32120  adjeq0  32123  dp2clq  32845  rpdp2cl  32846  dp2lt10  32848  dp2lt  32849  dp2ltc  32851  dplti  32869  zringfrac  33547  qqh0  33930  qqh1  33931  qqhcn  33937  rrh0  33961  esumcst  34027  esumrnmpt2  34032  volmeas  34195  hgt750lem  34628  tgoldbachgtde  34637  kur14lem7  35180  kur14lem9  35182  iinllyconn  35222  bj-rdg0gALT  37037  bj-pinftyccb  37187  bj-minftyccb  37191  bj-rrdrg  37256  finixpnum  37565  poimirlem32  37612  ftc1cnnclem  37651  ftc2nc  37662  areacirclem2  37669  prdsbnd  37753  reheibor  37799  rmxyadd  42878  rmxy1  42879  rmxy0  42880  rmydioph  42971  rmxdioph  42973  expdiophlem2  42979  expdioph  42980  mpaaeu  43107  0iscard  43503  1iscard  43504  fourierdlem85  46112  fourierdlem102  46129  fourierdlem114  46141  iooborel  46272  hoicvrrex  46477