Theorem sseldd 3185

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 3183	. 2 ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
4	1, 3	mpd 13	1 ⊢ (𝜑 → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2167   ⊆ wss 3157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  disjiun  4029  exmid01  4232  frirrg  4386  ordtri2or2exmid  4608  ontri2orexmidim  4609  riotass  5908  tfrcldm  6430  nntr2  6570  eroveu  6694  eroprf  6696  ixpssmapg  6796  findcard2d  6961  findcard2sd  6962  fimax2gtrilemstep  6970  undifdc  6994  fisseneq  7004  fidcenumlemrks  7028  fidcenumlemr  7030  fiuni  7053  suplub2ti  7076  ctssdclemn0  7185  acfun  7290  ccfunen  7347  nnppipi  7427  archnqq  7501  prarloclemlt  7577  suplocexprlemrl  7801  suplocexprlemmu  7802  suplocexprlemdisj  7804  suplocexprlemloc  7805  suplocexprlemex  7806  suplocexprlemub  7807  suplocexprlemlub  7808  suplocsrlemb  7890  suplocsrlempr  7891  suplocsrlem  7892  axpre-suploclemres  7985  suprubex  8995  suprzclex  9441  infregelbex  9689  fzssp1  10159  elfzoelz  10239  fzofzp1  10320  fzostep1  10330  zssinfcl  10339  suprzubdc  10343  zsupssdc  10345  suprzcl2dc  10346  frecuzrdgg  10525  frecuzrdgdomlem  10526  frecuzrdgsuctlem  10532  ser3mono  10596  seqf1oglem2a  10627  seqf1oglem2  10629  bcm1k  10869  fimaxq  10936  leisorel  10946  zfz1isolemiso  10948  seq3coll  10951  fimaxre2  11409  summodclem2a  11563  fsum3cvg3  11578  fsumcl2lem  11580  fsum0diaglem  11622  fsumiun  11659  prodmodclem2a  11758  fprodcl2lem  11787  fprodap0  11803  fprodrec  11811  fprodap0f  11818  fprodle  11822  bitsfzolem  12136  bitsfzo  12137  uzwodc  12229  4sqlemffi  12590  ennnfonelemhom  12657  exmidunben  12668  ctiunctlemfo  12681  nninfdclemcl  12690  nninfdclemp1  12692  nninfdclemlt  12693  nninfdclemf1  12694  unbendc  12696  strsetsid  12736  strslssd  12750  gsumpropd2  13095  gsumress  13097  resmhm  13189  mhmima  13193  grpidssd  13278  grpinvssd  13279  mulgnnsubcl  13340  mulgnn0subcl  13341  mulgsubcl  13342  mulgpropdg  13370  submmulg  13372  subg0  13386  subgsubcl  13391  subgsub  13392  subgmulg  13394  issubg4m  13399  nsgconj  13412  ssnmz  13417  ghmnsgima  13474  subgabl  13538  rdivmuldivd  13776  rhmunitinv  13810  subrguss  13868  subrginv  13869  subrgdv  13870  lsselg  13993  islss3  14011  lspsnel3  14037  lsspropdg  14063  rnglidlmcl  14112  znf1o  14283  topssnei  14482  cnprcl2k  14526  cnss1  14546  cnptopresti  14558  cnptoprest  14559  lmres  14568  txopn  14585  txcnp  14591  xmetres2  14699  blin2  14752  blopn  14810  xmettxlem  14829  xmettx  14830  elcncf2  14894  cncfmet  14912  cncfmptc  14916  cncfmptid  14917  negcncf  14925  mulcncflem  14927  cnrehmeocntop  14930  dedekindeulemuub  14937  dedekindeulemlu  14941  suplociccreex  14944  suplociccex  14945  dedekindicclemuub  14946  dedekindicclemlu  14950  dedekindicclemeu  14951  dedekindicclemicc  14952  ivthinclemlopn  14956  ivthinclemuopn  14958  ivthdec  14964  limcimolemlt  14984  cnplimcim  14987  cnplimclemle  14988  cnplimclemr  14989  cnlimci  14993  limccnpcntop  14995  limccnp2lem  14996  limccnp2cntop  14997  dvlemap  15000  dvfgg  15008  dvidsslem  15013  dvconstss  15018  dvcnp2cntop  15019  dvaddxxbr  15021  dvmulxxbr  15022  dvcoapbr  15027  dvcjbr  15028  plyf  15057  plycolemc  15078  dvply2g  15086  reeff1olem  15091  lgsquadlem3  15404  sssneq  15733