Theorem sselii 3905

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

This proof depends on syntax axioms:   ∈ wcel 2144   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-clel 2835  df-ss 3896

This theorem is used by:  sseliALT  5262  fvrn0  6914  ovima0  7601  brtpos0  8254  frrlem14  8321  rdg0  8433  iunfi  9336  rankdmr1  9813  rankeq0b  9880  cardprclem  10064  alephfp2  10192  dfac2b  10213  sdom2en01  10384  fin56  10475  fin1a2lem10  10491  hsmexlem4  10511  canthp1lem2  10742  ax1cn  11238  recni  11327  0xr  11360  pnfxr  11367  nn0rei  12621  nn0cni  12622  0xnn0  12689  nnzi  12724  nn0zi  12725  1q  13096  seqexw  14164  mulgfval  19285  lbsextlem4  21445  qsubdrg  21731  leordtval2  23536  iooordt  23541  hauspwdom  23826  comppfsc  23857  dfac14  23943  filconn  24208  isufil2  24233  iooretop  25090  ovolfiniun  25828  volfiniun  25874  iblabslem  26154  iblabs  26155  bddmulibl  26165  mdegcl  26393  0aa  26655  1aa  26656  iaa  26657  logcn  26981  logccv  26997  leibpi  27276  xrlimcnp  27302  jensen  27322  emre  27339  lgsdir2lem3  27660  shelii  31823  chelii  31841  omlsilem  32010  nonbooli  32259  pjssmii  32289  riesz4  32672  riesz1  32673  cnlnadjeu  32686  nmopadjlei  32696  adjeq0  32699  dp2clq  33494  rpdp2cl  33495  dp2lt10  33497  dp2lt  33498  dp2ltc  33500  dplti  33518  zringfrac  34133  vieta  34259  qqh0  34663  qqh1  34664  qqhcn  34670  rrh0  34694  esumcst  34742  esumrnmpt2  34747  volmeas  34911  hgt750lem  35327  tgoldbachgtde  35336  kur14lem7  36064  kur14lem9  36066  iinllyconn  36106  bj-rdg0gALT  38079  bj-pinftyccb  38236  bj-minftyccb  38240  bj-rrdrg  38305  finixpnum  38622  poimirlem32  38664  ftc1cnnclem  38703  ftc2nc  38714  areacirclem2  38721  prdsbnd  38821  reheibor  38867  rmxyadd  44022  rmxy1  44023  rmxy0  44024  rmydioph  44115  rmxdioph  44117  expdiophlem2  44123  expdioph  44124  mpaaeu  44246  0iscard  44636  1iscard  44637  wfaxrep  46078  wfaxnul  46080  wfaxinf2  46085  fourierdlem85  47295  fourierdlem102  47312  fourierdlem114  47324  iooborel  47455  hoicvrrex  47660  lamberte  48032