Theorem sseldd 3239

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 3237	. 2 |- ( ph -> ( C e. A -> C e. B ) )
4	1, 3	mpd 13	1 |- ( ph -> C e. B )

Syntax hints:   -> wi 4   e. wcel 2203   C_ wss 3211

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3217  df-ss 3224

This theorem is referenced by:  disjiun  4104  exmid01  4311  frirrg  4471  ordtri2or2exmid  4693  ontri2orexmidim  4694  riotass  6033  elovimad  6094  funsssuppss  6458  suppssfvg  6463  tfrcldm  6594  nntr2  6736  eroveu  6860  eroprf  6862  ixpssmapg  6963  findcard2d  7148  findcard2sd  7149  fimax2gtrilemstep  7158  elssdc  7162  eqsndc  7163  undifdc  7184  fisseneq  7195  fissfi  7216  fidcenumlemrks  7223  fidcenumlemr  7225  fiuni  7265  suplub2ti  7292  ctssdclemn0  7401  acfun  7514  ccfunen  7578  nnppipi  7658  archnqq  7732  prarloclemlt  7808  suplocexprlemrl  8032  suplocexprlemmu  8033  suplocexprlemdisj  8035  suplocexprlemloc  8036  suplocexprlemex  8037  suplocexprlemub  8038  suplocexprlemlub  8039  suplocsrlemb  8121  suplocsrlempr  8122  suplocsrlem  8123  axpre-suploclemres  8216  suprubex  9225  suprzclex  9676  infregelbex  9930  fzssp1  10401  elfzoelz  10481  fzofzp1  10572  fzostep1  10583  zssinfcl  10592  suprzubdc  10596  zsupssdc  10598  suprzcl2dc  10599  frecuzrdgg  10778  frecuzrdgdomlem  10779  frecuzrdgsuctlem  10785  ser3mono  10849  seqf1oglem2a  10880  seqf1oglem2  10882  bcm1k  11122  fimaxq  11194  leisorel  11209  zfz1isolemiso  11211  seq3coll  11214  fun2dmnop0  11222  swrdclg  11342  fimaxre2  11912  summodclem2a  12067  fsum3cvg3  12082  fsumcl2lem  12084  fsum0diaglem  12126  fsumiun  12163  prodmodclem2a  12262  fprodcl2lem  12291  fprodap0  12307  fprodrec  12315  fprodap0f  12322  fprodle  12326  bitsfzolem  12640  bitsfzo  12641  uzwodc  12733  4sqlemffi  13094  ennnfonelemhom  13166  exmidunben  13177  ctiunctlemfo  13190  nninfdclemcl  13199  nninfdclemp1  13201  nninfdclemlt  13202  nninfdclemf1  13203  unbendc  13205  strsetsid  13245  strslssd  13259  gsumpropd2  13606  gsumress  13608  resmhm  13700  mhmima  13704  grpidssd  13789  grpinvssd  13790  mulgnnsubcl  13851  mulgnn0subcl  13852  mulgsubcl  13853  mulgpropdg  13881  submmulg  13883  subg0  13897  subgsubcl  13902  subgsub  13903  subgmulg  13905  issubg4m  13910  nsgconj  13923  ssnmz  13928  ghmnsgima  13985  subgabl  14049  rdivmuldivd  14289  rhmunitinv  14323  subrguss  14381  subrginv  14382  subrgdv  14383  lsselg  14509  islss3  14527  lspsnel3  14553  lsspropdg  14579  rnglidlmcl  14628  znf1o  14799  topssnei  15027  cnprcl2k  15071  cnss1  15091  cnptopresti  15103  cnptoprest  15104  lmres  15113  txopn  15130  txcnp  15136  xmetres2  15244  blin2  15297  blopn  15355  xmettxlem  15374  xmettx  15375  elcncf2  15439  cncfmet  15457  cncfmptc  15461  cncfmptid  15462  negcncf  15470  mulcncflem  15472  cnrehmeocntop  15475  dedekindeulemuub  15482  dedekindeulemlu  15486  suplociccreex  15489  suplociccex  15490  dedekindicclemuub  15491  dedekindicclemlu  15495  dedekindicclemeu  15496  dedekindicclemicc  15497  ivthinclemlopn  15501  ivthinclemuopn  15503  ivthdec  15509  limcimolemlt  15529  cnplimcim  15532  cnplimclemle  15533  cnplimclemr  15534  cnlimci  15538  limccnpcntop  15540  limccnp2lem  15541  limccnp2cntop  15542  dvlemap  15545  dvfgg  15553  dvidsslem  15558  dvconstss  15563  dvcnp2cntop  15564  dvaddxxbr  15566  dvmulxxbr  15567  dvcoapbr  15572  dvcjbr  15573  plyf  15602  plycolemc  15623  dvply2g  15631  reeff1olem  15636  lgsquadlem3  15952  upgrex  16098  upgr1een  16119  subgruhgredgdm  16265  1hegrvtxdg1fi  16304  wlkvtxiedg  16340  wlkvtxiedgg  16341  sssneq  16776