Theorem sselii 3935

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

This proof depends on syntax axioms:   ∈ wcel 2146   ⊆ wss 3906

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 2148

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

This theorem is used by:  sseliALT  5274  fvrn0  6913  ovima0  7595  brtpos0  8231  frrlem14  8298  rdg0  8410  iunfi  9303  rankdmr1  9776  rankeq0b  9835  cardprclem  9977  alephfp2  10105  dfac2b  10126  sdom2en01  10297  fin56  10388  fin1a2lem10  10404  hsmexlem4  10424  canthp1lem2  10649  ax1cn  11145  recni  11234  0xr  11267  pnfxr  11274  nn0rei  12526  nn0cni  12527  0xnn0  12594  nnzi  12629  nn0zi  12630  seqexw  14067  mulgfval  19159  lbsextlem4  21315  qsubdrg  21599  leordtval2  23399  iooordt  23404  hauspwdom  23689  comppfsc  23720  dfac14  23806  filconn  24071  isufil2  24096  iooretop  24953  ovolfiniun  25691  volfiniun  25737  iblabslem  26018  iblabs  26019  bddmulibl  26029  mdegcl  26257  0aa  26517  1aa  26518  logcn  26843  logccv  26859  leibpi  27138  xrlimcnp  27164  jensen  27184  emre  27201  lgsdir2lem3  27522  shelii  31614  chelii  31632  omlsilem  31801  nonbooli  32050  pjssmii  32080  riesz4  32463  riesz1  32464  cnlnadjeu  32477  nmopadjlei  32487  adjeq0  32490  dp2clq  33246  rpdp2cl  33247  dp2lt10  33249  dp2lt  33250  dp2ltc  33252  dplti  33270  zringfrac  33884  vieta  34010  qqh0  34414  qqh1  34415  qqhcn  34421  rrh0  34445  esumcst  34493  esumrnmpt2  34498  volmeas  34662  hgt750lem  35079  tgoldbachgtde  35088  kur14lem7  35717  kur14lem9  35719  iinllyconn  35759  bj-rdg0gALT  37740  bj-pinftyccb  37898  bj-minftyccb  37902  bj-rrdrg  37967  finixpnum  38289  poimirlem32  38336  ftc1cnnclem  38375  ftc2nc  38386  areacirclem2  38393  prdsbnd  38477  reheibor  38523  rmxyadd  43681  rmxy1  43682  rmxy0  43683  rmydioph  43774  rmxdioph  43776  expdiophlem2  43782  expdioph  43783  mpaaeu  43910  0iscard  44300  1iscard  44301  wfaxrep  45736  wfaxnul  45738  wfaxinf2  45743  fourierdlem85  46938  fourierdlem102  46955  fourierdlem114  46967  iooborel  47098  hoicvrrex  47303  lamberte  47658