Theorem sselii 3960

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

Syntax hints:   ∈ wcel 2109   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2810  df-ss 3948

This theorem is referenced by:  sseliALT  5284  fvrn0  6911  ovima0  7591  brtpos0  8237  frrlem14  8303  wfrlem16OLD  8343  rdg0  8440  iunfi  9360  rankdmr1  9820  rankeq0b  9879  cardprclem  9998  alephfp2  10128  dfac2b  10150  sdom2en01  10321  fin56  10412  fin1a2lem10  10428  hsmexlem4  10448  canthp1lem2  10672  ax1cn  11168  recni  11254  0xr  11287  pnfxr  11294  nn0rei  12517  nn0cni  12518  0xnn0  12585  nnzi  12621  nn0zi  12622  seqexw  14040  mulgfval  19057  lbsextlem4  21127  qsubdrg  21392  leordtval2  23155  iooordt  23160  hauspwdom  23444  comppfsc  23475  dfac14  23561  filconn  23826  isufil2  23851  iooretop  24709  ovolfiniun  25459  volfiniun  25505  iblabslem  25786  iblabs  25787  bddmulibl  25797  mdegcl  26031  logcn  26613  logccv  26629  leibpi  26909  xrlimcnp  26935  jensen  26956  emre  26973  lgsdir2lem3  27295  shelii  31201  chelii  31219  omlsilem  31388  nonbooli  31637  pjssmii  31667  riesz4  32050  riesz1  32051  cnlnadjeu  32064  nmopadjlei  32074  adjeq0  32077  dp2clq  32860  rpdp2cl  32861  dp2lt10  32863  dp2lt  32864  dp2ltc  32866  dplti  32884  zringfrac  33574  qqh0  34020  qqh1  34021  qqhcn  34027  rrh0  34051  esumcst  34099  esumrnmpt2  34104  volmeas  34267  hgt750lem  34688  tgoldbachgtde  34697  kur14lem7  35239  kur14lem9  35241  iinllyconn  35281  bj-rdg0gALT  37094  bj-pinftyccb  37244  bj-minftyccb  37248  bj-rrdrg  37313  finixpnum  37634  poimirlem32  37681  ftc1cnnclem  37720  ftc2nc  37731  areacirclem2  37738  prdsbnd  37822  reheibor  37868  rmxyadd  42912  rmxy1  42913  rmxy0  42914  rmydioph  43005  rmxdioph  43007  expdiophlem2  43013  expdioph  43014  mpaaeu  43141  0iscard  43532  1iscard  43533  wfaxrep  44986  wfaxnul  44988  wfaxinf2  44993  fourierdlem85  46187  fourierdlem102  46204  fourierdlem114  46216  iooborel  46347  hoicvrrex  46552  lamberte  46887