Theorem sseldd 3205

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

Syntax hints:   → wi 4   ∈ wcel 2180   ⊆ wss 3177

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 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-11 1532  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-in 3183  df-ss 3190

This theorem is referenced by:  disjiun  4057  exmid01  4261  frirrg  4418  ordtri2or2exmid  4640  ontri2orexmidim  4641  riotass  5957  tfrcldm  6479  nntr2  6619  eroveu  6743  eroprf  6745  ixpssmapg  6845  findcard2d  7021  findcard2sd  7022  fimax2gtrilemstep  7030  undifdc  7054  fisseneq  7064  fidcenumlemrks  7088  fidcenumlemr  7090  fiuni  7113  suplub2ti  7136  ctssdclemn0  7245  acfun  7357  ccfunen  7418  nnppipi  7498  archnqq  7572  prarloclemlt  7648  suplocexprlemrl  7872  suplocexprlemmu  7873  suplocexprlemdisj  7875  suplocexprlemloc  7876  suplocexprlemex  7877  suplocexprlemub  7878  suplocexprlemlub  7879  suplocsrlemb  7961  suplocsrlempr  7962  suplocsrlem  7963  axpre-suploclemres  8056  suprubex  9066  suprzclex  9513  infregelbex  9761  fzssp1  10231  elfzoelz  10311  fzofzp1  10400  fzostep1  10410  zssinfcl  10419  suprzubdc  10423  zsupssdc  10425  suprzcl2dc  10426  frecuzrdgg  10605  frecuzrdgdomlem  10606  frecuzrdgsuctlem  10612  ser3mono  10676  seqf1oglem2a  10707  seqf1oglem2  10709  bcm1k  10949  fimaxq  11016  leisorel  11026  zfz1isolemiso  11028  seq3coll  11031  fun2dmnop0  11036  swrdclg  11148  fimaxre2  11704  summodclem2a  11858  fsum3cvg3  11873  fsumcl2lem  11875  fsum0diaglem  11917  fsumiun  11954  prodmodclem2a  12053  fprodcl2lem  12082  fprodap0  12098  fprodrec  12106  fprodap0f  12113  fprodle  12117  bitsfzolem  12431  bitsfzo  12432  uzwodc  12524  4sqlemffi  12885  ennnfonelemhom  12952  exmidunben  12963  ctiunctlemfo  12976  nninfdclemcl  12985  nninfdclemp1  12987  nninfdclemlt  12988  nninfdclemf1  12989  unbendc  12991  strsetsid  13031  strslssd  13045  gsumpropd2  13392  gsumress  13394  resmhm  13486  mhmima  13490  grpidssd  13575  grpinvssd  13576  mulgnnsubcl  13637  mulgnn0subcl  13638  mulgsubcl  13639  mulgpropdg  13667  submmulg  13669  subg0  13683  subgsubcl  13688  subgsub  13689  subgmulg  13691  issubg4m  13696  nsgconj  13709  ssnmz  13714  ghmnsgima  13771  subgabl  13835  rdivmuldivd  14073  rhmunitinv  14107  subrguss  14165  subrginv  14166  subrgdv  14167  lsselg  14290  islss3  14308  lspsnel3  14334  lsspropdg  14360  rnglidlmcl  14409  znf1o  14580  topssnei  14801  cnprcl2k  14845  cnss1  14865  cnptopresti  14877  cnptoprest  14878  lmres  14887  txopn  14904  txcnp  14910  xmetres2  15018  blin2  15071  blopn  15129  xmettxlem  15148  xmettx  15149  elcncf2  15213  cncfmet  15231  cncfmptc  15235  cncfmptid  15236  negcncf  15244  mulcncflem  15246  cnrehmeocntop  15249  dedekindeulemuub  15256  dedekindeulemlu  15260  suplociccreex  15263  suplociccex  15264  dedekindicclemuub  15265  dedekindicclemlu  15269  dedekindicclemeu  15270  dedekindicclemicc  15271  ivthinclemlopn  15275  ivthinclemuopn  15277  ivthdec  15283  limcimolemlt  15303  cnplimcim  15306  cnplimclemle  15307  cnplimclemr  15308  cnlimci  15312  limccnpcntop  15314  limccnp2lem  15315  limccnp2cntop  15316  dvlemap  15319  dvfgg  15327  dvidsslem  15332  dvconstss  15337  dvcnp2cntop  15338  dvaddxxbr  15340  dvmulxxbr  15341  dvcoapbr  15346  dvcjbr  15347  plyf  15376  plycolemc  15397  dvply2g  15405  reeff1olem  15410  lgsquadlem3  15723  upgrex  15868  sssneq  16279