Theorem sseldd 3143

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

Syntax hints:   → wi 4   ∈ wcel 2136   ⊆ wss 3116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-in 3122  df-ss 3129

This theorem is referenced by:  disjiun  3977  exmid01  4177  frirrg  4328  ordtri2or2exmid  4548  ontri2orexmidim  4549  riotass  5825  tfrcldm  6331  nntr2  6471  eroveu  6592  eroprf  6594  ixpssmapg  6694  findcard2d  6857  findcard2sd  6858  fimax2gtrilemstep  6866  undifdc  6889  fisseneq  6897  fidcenumlemrks  6918  fidcenumlemr  6920  fiuni  6943  suplub2ti  6966  ctssdclemn0  7075  acfun  7163  ccfunen  7205  nnppipi  7284  archnqq  7358  prarloclemlt  7434  suplocexprlemrl  7658  suplocexprlemmu  7659  suplocexprlemdisj  7661  suplocexprlemloc  7662  suplocexprlemex  7663  suplocexprlemub  7664  suplocexprlemlub  7665  suplocsrlemb  7747  suplocsrlempr  7748  suplocsrlem  7749  axpre-suploclemres  7842  suprubex  8846  suprzclex  9289  infregelbex  9536  fzssp1  10002  elfzoelz  10082  fzofzp1  10162  fzostep1  10172  frecuzrdgg  10351  frecuzrdgdomlem  10352  frecuzrdgsuctlem  10358  ser3mono  10413  bcm1k  10673  fimaxq  10740  leisorel  10750  zfz1isolemiso  10752  seq3coll  10755  fimaxre2  11168  summodclem2a  11322  fsum3cvg3  11337  fsumcl2lem  11339  fsum0diaglem  11381  fsumiun  11418  prodmodclem2a  11517  fprodcl2lem  11546  fprodap0  11562  fprodrec  11570  fprodap0f  11577  fprodle  11581  zssinfcl  11881  suprzubdc  11885  zsupssdc  11887  suprzcl2dc  11888  uzwodc  11970  ennnfonelemhom  12348  exmidunben  12359  ctiunctlemfo  12372  nninfdclemcl  12381  nninfdclemp1  12383  nninfdclemlt  12384  nninfdclemf1  12385  unbendc  12387  strsetsid  12427  strslssd  12440  topssnei  12802  cnprcl2k  12846  cnss1  12866  cnptopresti  12878  cnptoprest  12879  lmres  12888  txopn  12905  txcnp  12911  xmetres2  13019  blin2  13072  blopn  13130  xmettxlem  13149  xmettx  13150  elcncf2  13201  cncfmet  13219  cncfmptc  13222  cncfmptid  13223  negcncf  13228  mulcncflem  13230  cnrehmeocntop  13233  dedekindeulemuub  13235  dedekindeulemlu  13239  suplociccreex  13242  suplociccex  13243  dedekindicclemuub  13244  dedekindicclemlu  13248  dedekindicclemeu  13249  dedekindicclemicc  13250  ivthinclemlopn  13254  ivthinclemuopn  13256  ivthdec  13262  limcimolemlt  13273  cnplimcim  13276  cnplimclemle  13277  cnplimclemr  13278  cnlimci  13282  limccnpcntop  13284  limccnp2lem  13285  limccnp2cntop  13286  dvlemap  13289  dvfgg  13297  dvcnp2cntop  13303  dvaddxxbr  13305  dvmulxxbr  13306  dvcoapbr  13311  dvcjbr  13312  reeff1olem  13332  sssneq  13882