Theorem sseldd 3048

Description: Membership inference from subclass relationship. (Contributed by NM, 14-Dec-2004.)

Hypotheses

Ref	Expression
sseld.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
sseldd.2	⊢ (𝜑 → 𝐶 ∈ 𝐴)

Assertion

Ref	Expression
sseldd	⊢ (𝜑 → 𝐶 ∈ 𝐵)

Proof of Theorem sseldd

Step	Hyp	Ref	Expression
1		sseldd.2	. 2 ⊢ (𝜑 → 𝐶 ∈ 𝐴)
2		sseld.1	. . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
3	2	sseld 3046	. 2 ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
4	1, 3	mpd 13	1 ⊢ (𝜑 → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 1448   ⊆ wss 3021

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-11 1452  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-in 3027  df-ss 3034

This theorem is referenced by:  disjiun  3870  exmid01  4061  frirrg  4210  ordtri2or2exmid  4424  riotass  5689  tfrcldm  6190  nntr2  6329  eroveu  6450  eroprf  6452  ixpssmapg  6552  findcard2d  6714  findcard2sd  6715  fimax2gtrilemstep  6723  undifdc  6741  fisseneq  6749  fidcenumlemrks  6769  fidcenumlemr  6771  suplub2ti  6803  ctssdclemn0  6910  nnppipi  7052  archnqq  7126  prarloclemlt  7202  suprubex  8567  suprzclex  9001  fzssp1  9688  elfzoelz  9765  fzofzp1  9845  fzostep1  9855  frecuzrdgg  10030  frecuzrdgdomlem  10031  frecuzrdgsuctlem  10037  ser3mono  10092  bcm1k  10347  fimaxq  10414  leisorel  10421  zfz1isolemiso  10423  seq3coll  10426  fimaxre2  10837  summodclem2a  10989  fsum3cvg3  11004  fsumcl2lem  11006  fsum0diaglem  11048  fsumiun  11085  zssinfcl  11436  ennnfonelemhom  11720  exmidunben  11731  strsetsid  11774  strslssd  11787  topssnei  12113  cnprcl2k  12156  cnss1  12176  cnptopresti  12188  cnptoprest  12189  lmres  12198  txopn  12215  txcnp  12221  xmetres2  12307  blin2  12360  blopn  12418  elcncf2  12474  cncfmet  12492  cncfmptc  12495  cncfmptid  12496  negcncf  12500  mulcncflem  12502  limcimolemlt  12513  cnplimcim  12516  cnlimci  12518  limccnpcntop  12520  dvlemap  12522  dvfgg  12530