Theorem sseldd 3226

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

Syntax hints:   → wi 4   ∈ wcel 2200   ⊆ wss 3198

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211

This theorem is referenced by:  disjiun  4081  exmid01  4286  frirrg  4445  ordtri2or2exmid  4667  ontri2orexmidim  4668  riotass  5996  elovimad  6057  tfrcldm  6524  nntr2  6666  eroveu  6790  eroprf  6792  ixpssmapg  6892  findcard2d  7075  findcard2sd  7076  fimax2gtrilemstep  7085  elssdc  7089  eqsndc  7090  undifdc  7111  fisseneq  7121  fidcenumlemrks  7146  fidcenumlemr  7148  fiuni  7171  suplub2ti  7194  ctssdclemn0  7303  acfun  7415  ccfunen  7476  nnppipi  7556  archnqq  7630  prarloclemlt  7706  suplocexprlemrl  7930  suplocexprlemmu  7931  suplocexprlemdisj  7933  suplocexprlemloc  7934  suplocexprlemex  7935  suplocexprlemub  7936  suplocexprlemlub  7937  suplocsrlemb  8019  suplocsrlempr  8020  suplocsrlem  8021  axpre-suploclemres  8114  suprubex  9124  suprzclex  9571  infregelbex  9825  fzssp1  10295  elfzoelz  10375  fzofzp1  10465  fzostep1  10476  zssinfcl  10485  suprzubdc  10489  zsupssdc  10491  suprzcl2dc  10492  frecuzrdgg  10671  frecuzrdgdomlem  10672  frecuzrdgsuctlem  10678  ser3mono  10742  seqf1oglem2a  10773  seqf1oglem2  10775  bcm1k  11015  fimaxq  11084  leisorel  11094  zfz1isolemiso  11096  seq3coll  11099  fun2dmnop0  11104  swrdclg  11224  fimaxre2  11781  summodclem2a  11935  fsum3cvg3  11950  fsumcl2lem  11952  fsum0diaglem  11994  fsumiun  12031  prodmodclem2a  12130  fprodcl2lem  12159  fprodap0  12175  fprodrec  12183  fprodap0f  12190  fprodle  12194  bitsfzolem  12508  bitsfzo  12509  uzwodc  12601  4sqlemffi  12962  ennnfonelemhom  13029  exmidunben  13040  ctiunctlemfo  13053  nninfdclemcl  13062  nninfdclemp1  13064  nninfdclemlt  13065  nninfdclemf1  13066  unbendc  13068  strsetsid  13108  strslssd  13122  gsumpropd2  13469  gsumress  13471  resmhm  13563  mhmima  13567  grpidssd  13652  grpinvssd  13653  mulgnnsubcl  13714  mulgnn0subcl  13715  mulgsubcl  13716  mulgpropdg  13744  submmulg  13746  subg0  13760  subgsubcl  13765  subgsub  13766  subgmulg  13768  issubg4m  13773  nsgconj  13786  ssnmz  13791  ghmnsgima  13848  subgabl  13912  rdivmuldivd  14151  rhmunitinv  14185  subrguss  14243  subrginv  14244  subrgdv  14245  lsselg  14368  islss3  14386  lspsnel3  14412  lsspropdg  14438  rnglidlmcl  14487  znf1o  14658  topssnei  14879  cnprcl2k  14923  cnss1  14943  cnptopresti  14955  cnptoprest  14956  lmres  14965  txopn  14982  txcnp  14988  xmetres2  15096  blin2  15149  blopn  15207  xmettxlem  15226  xmettx  15227  elcncf2  15291  cncfmet  15309  cncfmptc  15313  cncfmptid  15314  negcncf  15322  mulcncflem  15324  cnrehmeocntop  15327  dedekindeulemuub  15334  dedekindeulemlu  15338  suplociccreex  15341  suplociccex  15342  dedekindicclemuub  15343  dedekindicclemlu  15347  dedekindicclemeu  15348  dedekindicclemicc  15349  ivthinclemlopn  15353  ivthinclemuopn  15355  ivthdec  15361  limcimolemlt  15381  cnplimcim  15384  cnplimclemle  15385  cnplimclemr  15386  cnlimci  15390  limccnpcntop  15392  limccnp2lem  15393  limccnp2cntop  15394  dvlemap  15397  dvfgg  15405  dvidsslem  15410  dvconstss  15415  dvcnp2cntop  15416  dvaddxxbr  15418  dvmulxxbr  15419  dvcoapbr  15424  dvcjbr  15425  plyf  15454  plycolemc  15475  dvply2g  15483  reeff1olem  15488  lgsquadlem3  15801  upgrex  15947  upgr1een  15968  1hegrvtxdg1fi  16120  wlkvtxiedg  16156  wlkvtxiedgg  16157  sssneq  16553