Theorem sseldd 3184

Description: Membership inference from subclass relationship. (Contributed by NM, 14-Dec-2004.)

Hypotheses

Ref	Expression
sseld.1	|- ( ph -> A C_ B )
sseldd.2	|- ( ph -> C e. A )

Assertion

Ref	Expression
sseldd	|- ( ph -> C e. B )

Proof of Theorem sseldd

Step	Hyp	Ref	Expression
1		sseldd.2	. 2 |- ( ph -> C e. A )
2		sseld.1	. . 3 |- ( ph -> A C_ B )
3	2	sseld 3182	. 2 |- ( ph -> ( C e. A -> C e. B ) )
4	1, 3	mpd 13	1 |- ( ph -> C e. B )

Syntax hints:   -> wi 4   e. wcel 2167   C_ 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  4028  exmid01  4231  frirrg  4385  ordtri2or2exmid  4607  ontri2orexmidim  4608  riotass  5905  tfrcldm  6421  nntr2  6561  eroveu  6685  eroprf  6687  ixpssmapg  6787  findcard2d  6952  findcard2sd  6953  fimax2gtrilemstep  6961  undifdc  6985  fisseneq  6995  fidcenumlemrks  7019  fidcenumlemr  7021  fiuni  7044  suplub2ti  7067  ctssdclemn0  7176  acfun  7274  ccfunen  7331  nnppipi  7410  archnqq  7484  prarloclemlt  7560  suplocexprlemrl  7784  suplocexprlemmu  7785  suplocexprlemdisj  7787  suplocexprlemloc  7788  suplocexprlemex  7789  suplocexprlemub  7790  suplocexprlemlub  7791  suplocsrlemb  7873  suplocsrlempr  7874  suplocsrlem  7875  axpre-suploclemres  7968  suprubex  8978  suprzclex  9424  infregelbex  9672  fzssp1  10142  elfzoelz  10222  fzofzp1  10303  fzostep1  10313  zssinfcl  10322  suprzubdc  10326  zsupssdc  10328  suprzcl2dc  10329  frecuzrdgg  10508  frecuzrdgdomlem  10509  frecuzrdgsuctlem  10515  ser3mono  10579  seqf1oglem2a  10610  seqf1oglem2  10612  bcm1k  10852  fimaxq  10919  leisorel  10929  zfz1isolemiso  10931  seq3coll  10934  fimaxre2  11392  summodclem2a  11546  fsum3cvg3  11561  fsumcl2lem  11563  fsum0diaglem  11605  fsumiun  11642  prodmodclem2a  11741  fprodcl2lem  11770  fprodap0  11786  fprodrec  11794  fprodap0f  11801  fprodle  11805  bitsfzolem  12118  bitsfzo  12119  uzwodc  12204  4sqlemffi  12565  ennnfonelemhom  12632  exmidunben  12643  ctiunctlemfo  12656  nninfdclemcl  12665  nninfdclemp1  12667  nninfdclemlt  12668  nninfdclemf1  12669  unbendc  12671  strsetsid  12711  strslssd  12725  gsumpropd2  13036  gsumress  13038  resmhm  13119  mhmima  13123  grpidssd  13208  grpinvssd  13209  mulgnnsubcl  13264  mulgnn0subcl  13265  mulgsubcl  13266  mulgpropdg  13294  submmulg  13296  subg0  13310  subgsubcl  13315  subgsub  13316  subgmulg  13318  issubg4m  13323  nsgconj  13336  ssnmz  13341  ghmnsgima  13398  subgabl  13462  rdivmuldivd  13700  rhmunitinv  13734  subrguss  13792  subrginv  13793  subrgdv  13794  lsselg  13917  islss3  13935  lspsnel3  13961  lsspropdg  13987  rnglidlmcl  14036  znf1o  14207  topssnei  14398  cnprcl2k  14442  cnss1  14462  cnptopresti  14474  cnptoprest  14475  lmres  14484  txopn  14501  txcnp  14507  xmetres2  14615  blin2  14668  blopn  14726  xmettxlem  14745  xmettx  14746  elcncf2  14810  cncfmet  14828  cncfmptc  14832  cncfmptid  14833  negcncf  14841  mulcncflem  14843  cnrehmeocntop  14846  dedekindeulemuub  14853  dedekindeulemlu  14857  suplociccreex  14860  suplociccex  14861  dedekindicclemuub  14862  dedekindicclemlu  14866  dedekindicclemeu  14867  dedekindicclemicc  14868  ivthinclemlopn  14872  ivthinclemuopn  14874  ivthdec  14880  limcimolemlt  14900  cnplimcim  14903  cnplimclemle  14904  cnplimclemr  14905  cnlimci  14909  limccnpcntop  14911  limccnp2lem  14912  limccnp2cntop  14913  dvlemap  14916  dvfgg  14924  dvidsslem  14929  dvconstss  14934  dvcnp2cntop  14935  dvaddxxbr  14937  dvmulxxbr  14938  dvcoapbr  14943  dvcjbr  14944  plyf  14973  plycolemc  14994  dvply2g  15002  reeff1olem  15007  lgsquadlem3  15320  sssneq  15646