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  7292  ccfunen  7349  nnppipi  7429  archnqq  7503  prarloclemlt  7579  suplocexprlemrl  7803  suplocexprlemmu  7804  suplocexprlemdisj  7806  suplocexprlemloc  7807  suplocexprlemex  7808  suplocexprlemub  7809  suplocexprlemlub  7810  suplocsrlemb  7892  suplocsrlempr  7893  suplocsrlem  7894  axpre-suploclemres  7987  suprubex  8997  suprzclex  9443  infregelbex  9691  fzssp1  10161  elfzoelz  10241  fzofzp1  10322  fzostep1  10332  zssinfcl  10341  suprzubdc  10345  zsupssdc  10347  suprzcl2dc  10348  frecuzrdgg  10527  frecuzrdgdomlem  10528  frecuzrdgsuctlem  10534  ser3mono  10598  seqf1oglem2a  10629  seqf1oglem2  10631  bcm1k  10871  fimaxq  10938  leisorel  10948  zfz1isolemiso  10950  seq3coll  10953  fimaxre2  11411  summodclem2a  11565  fsum3cvg3  11580  fsumcl2lem  11582  fsum0diaglem  11624  fsumiun  11661  prodmodclem2a  11760  fprodcl2lem  11789  fprodap0  11805  fprodrec  11813  fprodap0f  11820  fprodle  11824  bitsfzolem  12138  bitsfzo  12139  uzwodc  12231  4sqlemffi  12592  ennnfonelemhom  12659  exmidunben  12670  ctiunctlemfo  12683  nninfdclemcl  12692  nninfdclemp1  12694  nninfdclemlt  12695  nninfdclemf1  12696  unbendc  12698  strsetsid  12738  strslssd  12752  gsumpropd2  13097  gsumress  13099  resmhm  13191  mhmima  13195  grpidssd  13280  grpinvssd  13281  mulgnnsubcl  13342  mulgnn0subcl  13343  mulgsubcl  13344  mulgpropdg  13372  submmulg  13374  subg0  13388  subgsubcl  13393  subgsub  13394  subgmulg  13396  issubg4m  13401  nsgconj  13414  ssnmz  13419  ghmnsgima  13476  subgabl  13540  rdivmuldivd  13778  rhmunitinv  13812  subrguss  13870  subrginv  13871  subrgdv  13872  lsselg  13995  islss3  14013  lspsnel3  14039  lsspropdg  14065  rnglidlmcl  14114  znf1o  14285  topssnei  14506  cnprcl2k  14550  cnss1  14570  cnptopresti  14582  cnptoprest  14583  lmres  14592  txopn  14609  txcnp  14615  xmetres2  14723  blin2  14776  blopn  14834  xmettxlem  14853  xmettx  14854  elcncf2  14918  cncfmet  14936  cncfmptc  14940  cncfmptid  14941  negcncf  14949  mulcncflem  14951  cnrehmeocntop  14954  dedekindeulemuub  14961  dedekindeulemlu  14965  suplociccreex  14968  suplociccex  14969  dedekindicclemuub  14970  dedekindicclemlu  14974  dedekindicclemeu  14975  dedekindicclemicc  14976  ivthinclemlopn  14980  ivthinclemuopn  14982  ivthdec  14988  limcimolemlt  15008  cnplimcim  15011  cnplimclemle  15012  cnplimclemr  15013  cnlimci  15017  limccnpcntop  15019  limccnp2lem  15020  limccnp2cntop  15021  dvlemap  15024  dvfgg  15032  dvidsslem  15037  dvconstss  15042  dvcnp2cntop  15043  dvaddxxbr  15045  dvmulxxbr  15046  dvcoapbr  15051  dvcjbr  15052  plyf  15081  plycolemc  15102  dvply2g  15110  reeff1olem  15115  lgsquadlem3  15428  sssneq  15757