Theorem sselii 3980

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

Syntax hints:   ∈ wcel 2107   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  sseliALT  5310  fvrn0  6922  ovima0  7586  brtpos0  8218  frrlem14  8284  wfrlem16OLD  8324  rdg0  8421  iunfi  9340  rankdmr1  9796  rankeq0b  9855  cardprclem  9974  alephfp2  10104  dfac2b  10125  sdom2en01  10297  fin56  10388  fin1a2lem10  10404  hsmexlem4  10424  canthp1lem2  10648  ax1cn  11144  recni  11228  0xr  11261  pnfxr  11268  nn0rei  12483  nn0cni  12484  0xnn0  12550  nnzi  12586  nn0zi  12587  seqexw  13982  mulgfval  18952  lbsextlem4  20774  qsubdrg  20997  leordtval2  22716  iooordt  22721  hauspwdom  23005  comppfsc  23036  dfac14  23122  filconn  23387  isufil2  23412  iooretop  24282  ovolfiniun  25018  volfiniun  25064  iblabslem  25345  iblabs  25346  bddmulibl  25356  mdegcl  25587  logcn  26155  logccv  26171  leibpi  26447  xrlimcnp  26473  jensen  26493  emre  26510  lgsdir2lem3  26830  shelii  30468  chelii  30486  omlsilem  30655  nonbooli  30904  pjssmii  30934  riesz4  31317  riesz1  31318  cnlnadjeu  31331  nmopadjlei  31341  adjeq0  31344  dp2clq  32047  rpdp2cl  32048  dp2lt10  32050  dp2lt  32051  dp2ltc  32053  dplti  32071  qqh0  32964  qqh1  32965  qqhcn  32971  rrh0  32995  esumcst  33061  esumrnmpt2  33066  volmeas  33229  hgt750lem  33663  tgoldbachgtde  33672  kur14lem7  34203  kur14lem9  34205  iinllyconn  34245  bj-rdg0gALT  35952  bj-pinftyccb  36102  bj-minftyccb  36106  bj-rrdrg  36171  finixpnum  36473  poimirlem32  36520  ftc1cnnclem  36559  ftc2nc  36570  areacirclem2  36577  prdsbnd  36661  reheibor  36707  rmxyadd  41660  rmxy1  41661  rmxy0  41662  rmydioph  41753  rmxdioph  41755  expdiophlem2  41761  expdioph  41762  mpaaeu  41892  0iscard  42292  1iscard  42293  fourierdlem85  44907  fourierdlem102  44924  fourierdlem114  44936  iooborel  45067  hoicvrrex  45272