Theorem sselii 3910

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

This proof depends on syntax axioms:   ∈ wcel 2147   ⊆ wss 3900

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 1945  ax-6 2002  ax-7 2043  ax-8 2149

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

This theorem is used by:  sseliALT  5267  fvrn0  6942  ovima0  7630  brtpos0  8286  frrlem14  8353  rdg0  8465  iunfi  9368  rankdmr1  9844  rankeq0b  9911  cardprclem  10095  alephfp2  10225  dfac2b  10246  sdom2en01  10417  fin56  10508  fin1a2lem10  10524  hsmexlem4  10544  canthp1lem2  10775  ax1cn  11271  recni  11360  0xr  11393  pnfxr  11400  nn0rei  12655  nn0cni  12656  0xnn0  12723  nnzi  12758  nn0zi  12759  1q  13130  seqexw  14198  mulgfval  19320  lbsextlem4  21481  qsubdrg  21769  leordtval2  23574  iooordt  23579  hauspwdom  23864  comppfsc  23895  dfac14  23981  filconn  24246  isufil2  24271  iooretop  25128  ovolfiniun  25866  volfiniun  25912  iblabslem  26192  iblabs  26193  bddmulibl  26203  mdegcl  26431  0aa  26695  1aa  26696  iaa  26697  logcn  27021  logccv  27037  leibpi  27316  xrlimcnp  27342  jensen  27362  emre  27379  lgsdir2lem3  27700  shelii  31863  chelii  31881  omlsilem  32050  nonbooli  32299  pjssmii  32329  riesz4  32712  riesz1  32713  cnlnadjeu  32726  nmopadjlei  32736  adjeq0  32739  dp2clq  33533  rpdp2cl  33534  dp2lt10  33536  dp2lt  33537  dp2ltc  33539  dplti  33557  zringfrac  34182  vieta  34316  qqh0  34720  qqh1  34721  qqhcn  34727  rrh0  34751  esumcst  34799  esumrnmpt2  34804  volmeas  34968  hgt750lem  35384  tgoldbachgtde  35393  kur14lem7  36178  kur14lem9  36180  iinllyconn  36220  bj-rdg0gALT  38249  bj-pinftyccb  38403  bj-minftyccb  38407  bj-rrdrg  38472  finixpnum  38789  poimirlem32  38831  ftc1cnnclem  38870  ftc2nc  38881  areacirclem2  38888  prdsbnd  38986  reheibor  39032  rmxyadd  44188  rmxy1  44189  rmxy0  44190  rmydioph  44281  rmxdioph  44283  expdiophlem2  44289  expdioph  44290  mpaaeu  44411  0iscard  44797  1iscard  44798  wfaxrep  46242  wfaxnul  46244  wfaxinf2  46249  fourierdlem85  47468  fourierdlem102  47485  fourierdlem114  47497  iooborel  47628  hoicvrrex  47833  lamberte  48205