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 2836  df-ss 3916

This theorem is used by:  sseliALT  5263  fvrn0  6911  ovima0  7598  brtpos0  8243  frrlem14  8310  rdg0  8422  iunfi  9325  rankdmr1  9802  rankeq0b  9869  cardprclem  10053  alephfp2  10181  dfac2b  10202  sdom2en01  10373  fin56  10464  fin1a2lem10  10480  hsmexlem4  10500  canthp1lem2  10731  ax1cn  11227  recni  11316  0xr  11349  pnfxr  11356  nn0rei  12610  nn0cni  12611  0xnn0  12678  nnzi  12713  nn0zi  12714  1q  13085  seqexw  14153  mulgfval  19272  lbsextlem4  21432  qsubdrg  21718  leordtval2  23523  iooordt  23528  hauspwdom  23813  comppfsc  23844  dfac14  23930  filconn  24195  isufil2  24220  iooretop  25077  ovolfiniun  25815  volfiniun  25861  iblabslem  26141  iblabs  26142  bddmulibl  26152  mdegcl  26380  0aa  26642  1aa  26643  iaa  26644  logcn  26968  logccv  26984  leibpi  27263  xrlimcnp  27289  jensen  27309  emre  27326  lgsdir2lem3  27647  shelii  31810  chelii  31828  omlsilem  31997  nonbooli  32246  pjssmii  32276  riesz4  32659  riesz1  32660  cnlnadjeu  32673  nmopadjlei  32683  adjeq0  32686  dp2clq  33440  rpdp2cl  33441  dp2lt10  33443  dp2lt  33444  dp2ltc  33446  dplti  33464  zringfrac  34079  vieta  34205  qqh0  34609  qqh1  34610  qqhcn  34616  rrh0  34640  esumcst  34688  esumrnmpt2  34693  volmeas  34857  hgt750lem  35273  tgoldbachgtde  35282  kur14lem7  35956  kur14lem9  35958  iinllyconn  35998  bj-rdg0gALT  37966  bj-pinftyccb  38122  bj-minftyccb  38126  bj-rrdrg  38191  finixpnum  38508  poimirlem32  38550  ftc1cnnclem  38589  ftc2nc  38600  areacirclem2  38607  prdsbnd  38707  reheibor  38753  rmxyadd  43907  rmxy1  43908  rmxy0  43909  rmydioph  44000  rmxdioph  44002  expdiophlem2  44008  expdioph  44009  mpaaeu  44136  0iscard  44526  1iscard  44527  wfaxrep  45962  wfaxnul  45964  wfaxinf2  45969  fourierdlem85  47170  fourierdlem102  47187  fourierdlem114  47199  iooborel  47330  hoicvrrex  47535  lamberte  47907