Theorem sselii 3892

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

Syntax hints:   ∈ wcel 2083   ⊆ wss 3865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-in 3872  df-ss 3880

This theorem is referenced by:  sseliALT  5111  fvrn0  6573  ovima0  7190  brtpos0  7757  wfrlem16  7829  rdg0  7916  iunfi  8665  rankdmr1  9083  rankeq0b  9142  cardprclem  9261  alephfp2  9388  dfac2b  9409  sdom2en01  9577  fin56  9668  fin1a2lem10  9684  hsmexlem4  9704  canthp1lem2  9928  ax1cn  10424  recni  10508  0xr  10541  pnfxr  10548  nn0rei  11762  nn0cni  11763  0xnn0  11827  nnzi  11860  nn0zi  11861  seqexw  13239  mulgfval  17987  lbsextlem4  19627  qsubdrg  20283  leordtval2  21508  iooordt  21513  hauspwdom  21797  comppfsc  21828  dfac14  21914  filconn  22179  isufil2  22204  iooretop  23061  ovolfiniun  23789  volfiniun  23835  iblabslem  24115  iblabs  24116  bddmulibl  24126  mdegcl  24350  logcn  24915  logccv  24931  leibpi  25206  xrlimcnp  25232  jensen  25252  emre  25269  lgsdir2lem3  25589  shelii  28679  chelii  28697  omlsilem  28866  nonbooli  29115  pjssmii  29145  riesz4  29528  riesz1  29529  cnlnadjeu  29542  nmopadjlei  29552  adjeq0  29555  dp2clq  30237  rpdp2cl  30238  dp2lt10  30240  dp2lt  30241  dp2ltc  30243  dplti  30261  qqh0  30838  qqh1  30839  qqhcn  30845  rrh0  30869  esumcst  30935  esumrnmpt2  30940  volmeas  31103  hgt750lem  31535  tgoldbachgtde  31544  kur14lem7  32069  kur14lem9  32071  iinllyconn  32111  frrlem14  32747  bj-pinftyccb  34082  bj-minftyccb  34086  finixpnum  34429  poimirlem32  34476  ftc1cnnclem  34517  ftc2nc  34528  areacirclem2  34535  prdsbnd  34624  reheibor  34670  rmxyadd  39024  rmxy1  39025  rmxy0  39026  rmydioph  39117  rmxdioph  39119  expdiophlem2  39125  expdioph  39126  mpaaeu  39256  fourierdlem85  42040  fourierdlem102  42057  fourierdlem114  42069  iooborel  42198  hoicvrrex  42402