Theorem sselii 3928

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

This proof depends on syntax axioms:   ∈ wcel 2145   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2835  df-ss 3916

This theorem is used by:  sseliALT  5266  fvrn0  6906  ovima0  7593  brtpos0  8231  frrlem14  8298  rdg0  8410  iunfi  9310  rankdmr1  9783  rankeq0b  9842  cardprclem  9984  alephfp2  10112  dfac2b  10133  sdom2en01  10304  fin56  10395  fin1a2lem10  10411  hsmexlem4  10431  canthp1lem2  10662  ax1cn  11158  recni  11247  0xr  11280  pnfxr  11287  nn0rei  12539  nn0cni  12540  0xnn0  12607  nnzi  12642  nn0zi  12643  1q  13014  seqexw  14081  mulgfval  19192  lbsextlem4  21348  qsubdrg  21632  leordtval2  23437  iooordt  23442  hauspwdom  23727  comppfsc  23758  dfac14  23844  filconn  24109  isufil2  24134  iooretop  24991  ovolfiniun  25729  volfiniun  25775  iblabslem  26055  iblabs  26056  bddmulibl  26066  mdegcl  26294  0aa  26558  1aa  26559  iaa  26560  logcn  26884  logccv  26900  leibpi  27179  xrlimcnp  27205  jensen  27225  emre  27242  lgsdir2lem3  27563  shelii  31696  chelii  31714  omlsilem  31883  nonbooli  32132  pjssmii  32162  riesz4  32545  riesz1  32546  cnlnadjeu  32559  nmopadjlei  32569  adjeq0  32572  dp2clq  33326  rpdp2cl  33327  dp2lt10  33329  dp2lt  33330  dp2ltc  33332  dplti  33350  zringfrac  33964  vieta  34090  qqh0  34494  qqh1  34495  qqhcn  34501  rrh0  34525  esumcst  34573  esumrnmpt2  34578  volmeas  34742  hgt750lem  35159  tgoldbachgtde  35168  kur14lem7  35791  kur14lem9  35793  iinllyconn  35833  bj-rdg0gALT  37815  bj-pinftyccb  37973  bj-minftyccb  37977  bj-rrdrg  38042  finixpnum  38359  poimirlem32  38401  ftc1cnnclem  38440  ftc2nc  38451  areacirclem2  38458  prdsbnd  38543  reheibor  38589  rmxyadd  43762  rmxy1  43763  rmxy0  43764  rmydioph  43855  rmxdioph  43857  expdiophlem2  43863  expdioph  43864  mpaaeu  43991  0iscard  44381  1iscard  44382  wfaxrep  45817  wfaxnul  45819  wfaxinf2  45824  fourierdlem85  47019  fourierdlem102  47036  fourierdlem114  47048  iooborel  47179  hoicvrrex  47384  lamberte  47756