Theorem sseldd 3156

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

Syntax hints:   → wi 4   ∈ wcel 2148   ⊆ wss 3129

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142

This theorem is referenced by:  disjiun  3995  exmid01  4195  frirrg  4346  ordtri2or2exmid  4566  ontri2orexmidim  4567  riotass  5851  tfrcldm  6357  nntr2  6497  eroveu  6619  eroprf  6621  ixpssmapg  6721  findcard2d  6884  findcard2sd  6885  fimax2gtrilemstep  6893  undifdc  6916  fisseneq  6924  fidcenumlemrks  6945  fidcenumlemr  6947  fiuni  6970  suplub2ti  6993  ctssdclemn0  7102  acfun  7199  ccfunen  7241  nnppipi  7320  archnqq  7394  prarloclemlt  7470  suplocexprlemrl  7694  suplocexprlemmu  7695  suplocexprlemdisj  7697  suplocexprlemloc  7698  suplocexprlemex  7699  suplocexprlemub  7700  suplocexprlemlub  7701  suplocsrlemb  7783  suplocsrlempr  7784  suplocsrlem  7785  axpre-suploclemres  7878  suprubex  8884  suprzclex  9327  infregelbex  9574  fzssp1  10040  elfzoelz  10120  fzofzp1  10200  fzostep1  10210  frecuzrdgg  10389  frecuzrdgdomlem  10390  frecuzrdgsuctlem  10396  ser3mono  10451  bcm1k  10711  fimaxq  10778  leisorel  10788  zfz1isolemiso  10790  seq3coll  10793  fimaxre2  11206  summodclem2a  11360  fsum3cvg3  11375  fsumcl2lem  11377  fsum0diaglem  11419  fsumiun  11456  prodmodclem2a  11555  fprodcl2lem  11584  fprodap0  11600  fprodrec  11608  fprodap0f  11615  fprodle  11619  zssinfcl  11919  suprzubdc  11923  zsupssdc  11925  suprzcl2dc  11926  uzwodc  12008  ennnfonelemhom  12386  exmidunben  12397  ctiunctlemfo  12410  nninfdclemcl  12419  nninfdclemp1  12421  nninfdclemlt  12422  nninfdclemf1  12423  unbendc  12425  strsetsid  12465  strslssd  12478  mhmima  12752  grpidssd  12822  grpinvssd  12823  mulgnnsubcl  12871  mulgnn0subcl  12872  mulgsubcl  12873  mulgpropdg  12900  topssnei  13295  cnprcl2k  13339  cnss1  13359  cnptopresti  13371  cnptoprest  13372  lmres  13381  txopn  13398  txcnp  13404  xmetres2  13512  blin2  13565  blopn  13623  xmettxlem  13642  xmettx  13643  elcncf2  13694  cncfmet  13712  cncfmptc  13715  cncfmptid  13716  negcncf  13721  mulcncflem  13723  cnrehmeocntop  13726  dedekindeulemuub  13728  dedekindeulemlu  13732  suplociccreex  13735  suplociccex  13736  dedekindicclemuub  13737  dedekindicclemlu  13741  dedekindicclemeu  13742  dedekindicclemicc  13743  ivthinclemlopn  13747  ivthinclemuopn  13749  ivthdec  13755  limcimolemlt  13766  cnplimcim  13769  cnplimclemle  13770  cnplimclemr  13771  cnlimci  13775  limccnpcntop  13777  limccnp2lem  13778  limccnp2cntop  13779  dvlemap  13782  dvfgg  13790  dvcnp2cntop  13796  dvaddxxbr  13798  dvmulxxbr  13799  dvcoapbr  13804  dvcjbr  13805  reeff1olem  13825  sssneq  14374