Theorem sselii 3926

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

This proof depends on syntax axioms:   ∈ wcel 2145   ⊆ wss 3914

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 3915

This theorem is used by:  sseliALT  5263  fvrn0  6914  ovima0  7601  brtpos0  8251  frrlem14  8318  rdg0  8430  iunfi  9333  rankdmr1  9810  rankeq0b  9877  cardprclem  10061  alephfp2  10189  dfac2b  10210  sdom2en01  10381  fin56  10472  fin1a2lem10  10488  hsmexlem4  10508  canthp1lem2  10739  ax1cn  11235  recni  11324  0xr  11357  pnfxr  11364  nn0rei  12618  nn0cni  12619  0xnn0  12686  nnzi  12721  nn0zi  12722  1q  13093  seqexw  14161  mulgfval  19280  lbsextlem4  21440  qsubdrg  21726  leordtval2  23531  iooordt  23536  hauspwdom  23821  comppfsc  23852  dfac14  23938  filconn  24203  isufil2  24228  iooretop  25085  ovolfiniun  25823  volfiniun  25869  iblabslem  26149  iblabs  26150  bddmulibl  26160  mdegcl  26388  0aa  26650  1aa  26651  iaa  26652  logcn  26976  logccv  26992  leibpi  27271  xrlimcnp  27297  jensen  27317  emre  27334  lgsdir2lem3  27655  shelii  31818  chelii  31836  omlsilem  32005  nonbooli  32254  pjssmii  32284  riesz4  32667  riesz1  32668  cnlnadjeu  32681  nmopadjlei  32691  adjeq0  32694  dp2clq  33448  rpdp2cl  33449  dp2lt10  33451  dp2lt  33452  dp2ltc  33454  dplti  33472  zringfrac  34087  vieta  34213  qqh0  34617  qqh1  34618  qqhcn  34624  rrh0  34648  esumcst  34696  esumrnmpt2  34701  volmeas  34865  hgt750lem  35281  tgoldbachgtde  35290  kur14lem7  35978  kur14lem9  35980  iinllyconn  36020  bj-rdg0gALT  37987  bj-pinftyccb  38144  bj-minftyccb  38148  bj-rrdrg  38213  finixpnum  38530  poimirlem32  38572  ftc1cnnclem  38611  ftc2nc  38622  areacirclem2  38629  prdsbnd  38729  reheibor  38775  rmxyadd  43929  rmxy1  43930  rmxy0  43931  rmydioph  44022  rmxdioph  44024  expdiophlem2  44030  expdioph  44031  mpaaeu  44153  0iscard  44543  1iscard  44544  wfaxrep  45985  wfaxnul  45987  wfaxinf2  45992  fourierdlem85  47202  fourierdlem102  47219  fourierdlem114  47231  iooborel  47362  hoicvrrex  47567  lamberte  47939