Theorem sselii 3942

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

Syntax hints:   ∈ wcel 2149   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-clel 2844  df-ss 3930

This theorem is referenced by:  sseliALT  5271  fvrn0  6907  ovima0  7587  brtpos0  8225  frrlem14  8292  rdg0  8404  iunfi  9296  rankdmr1  9769  rankeq0b  9828  cardprclem  9961  alephfp2  10089  dfac2b  10110  sdom2en01  10282  fin56  10373  fin1a2lem10  10389  hsmexlem4  10409  canthp1lem2  10634  ax1cn  11130  recni  11219  0xr  11252  pnfxr  11259  nn0rei  12511  nn0cni  12512  0xnn0  12579  nnzi  12614  nn0zi  12615  seqexw  14049  mulgfval  19131  lbsextlem4  21259  qsubdrg  21534  leordtval2  23334  iooordt  23339  hauspwdom  23623  comppfsc  23654  dfac14  23740  filconn  24005  isufil2  24030  iooretop  24887  ovolfiniun  25625  volfiniun  25671  iblabslem  25952  iblabs  25953  bddmulibl  25963  mdegcl  26191  logcn  26774  logccv  26790  leibpi  27069  xrlimcnp  27095  jensen  27115  emre  27132  lgsdir2lem3  27453  shelii  31504  chelii  31522  omlsilem  31691  nonbooli  31940  pjssmii  31970  riesz4  32353  riesz1  32354  cnlnadjeu  32367  nmopadjlei  32377  adjeq0  32380  dp2clq  33137  rpdp2cl  33138  dp2lt10  33140  dp2lt  33141  dp2ltc  33143  dplti  33161  zringfrac  33785  vieta  33911  qqh0  34315  qqh1  34316  qqhcn  34322  rrh0  34346  esumcst  34394  esumrnmpt2  34399  volmeas  34562  hgt750lem  34979  tgoldbachgtde  34988  kur14lem7  35599  kur14lem9  35601  iinllyconn  35641  bj-rdg0gALT  37591  bj-pinftyccb  37748  bj-minftyccb  37752  bj-rrdrg  37817  finixpnum  38139  poimirlem32  38186  ftc1cnnclem  38225  ftc2nc  38236  areacirclem2  38243  prdsbnd  38327  reheibor  38373  rmxyadd  43533  rmxy1  43534  rmxy0  43535  rmydioph  43626  rmxdioph  43628  expdiophlem2  43634  expdioph  43635  mpaaeu  43762  0iscard  44152  1iscard  44153  wfaxrep  45588  wfaxnul  45590  wfaxinf2  45595  fourierdlem85  46790  fourierdlem102  46807  fourierdlem114  46819  iooborel  46950  hoicvrrex  47155  lamberte  47507