Theorem sseldd 3243

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

Syntax hints:   -> wi 4   e. wcel 2205   C_ wss 3214

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 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  disjiun  4109  exmid01  4316  frirrg  4476  ordtri2or2exmid  4698  ontri2orexmidim  4699  riotass  6041  elovimad  6102  funsssuppss  6471  suppssfvg  6476  tfrcldm  6607  nntr2  6749  eroveu  6873  eroprf  6875  ixpssmapg  6976  findcard2d  7161  findcard2sd  7162  fimax2gtrilemstep  7171  elssdc  7175  eqsndc  7176  undifdc  7197  fisseneq  7208  fissfi  7229  fidcenumlemrks  7236  fidcenumlemr  7238  fiuni  7278  suplub2ti  7305  ctssdclemn0  7414  acfun  7527  ccfunen  7594  nnppipi  7674  archnqq  7748  prarloclemlt  7824  suplocexprlemrl  8048  suplocexprlemmu  8049  suplocexprlemdisj  8051  suplocexprlemloc  8052  suplocexprlemex  8053  suplocexprlemub  8054  suplocexprlemlub  8055  suplocsrlemb  8137  suplocsrlempr  8138  suplocsrlem  8139  axpre-suploclemres  8232  suprubex  9242  suprzclex  9694  infregelbex  9948  fzssp1  10422  elfzoelz  10503  fzofzp1  10594  fzostep1  10605  zssinfcl  10614  suprzubdc  10620  zsupssdc  10622  suprzcl2dc  10623  frecuzrdgg  10802  frecuzrdgdomlem  10803  frecuzrdgsuctlem  10809  ser3mono  10873  seqf1oglem2a  10904  seqf1oglem2  10906  bcm1k  11147  fimaxq  11219  leisorel  11234  zfz1isolemiso  11236  seq3coll  11239  fun2dmnop0  11247  swrdclg  11367  fimaxre2  11937  summodclem2a  12092  fsum3cvg3  12107  fsumcl2lem  12109  fsum0diaglem  12151  fsumiun  12188  prodmodclem2a  12287  fprodcl2lem  12316  fprodap0  12332  fprodrec  12340  fprodap0f  12347  fprodle  12351  bitsfzolem  12665  bitsfzo  12666  uzwodc  12758  4sqlemffi  13119  ballotfilemcdc  13167  ballotfilemsdom  13199  ballotfilemfrceq  13216  ennnfonelemhom  13250  exmidunben  13261  ctiunctlemfo  13274  nninfdclemcl  13283  nninfdclemp1  13285  nninfdclemlt  13286  nninfdclemf1  13287  unbendc  13289  strsetsid  13329  strslssd  13343  gsumpropd2  13656  gsumress  13658  resmhm  13742  mhmima  13746  grpidssd  13831  grpinvssd  13832  mulgnnsubcl  13887  mulgnn0subcl  13888  mulgsubcl  13889  mulgpropdg  13917  submmulg  13919  subg0  13933  subgsubcl  13938  subgsub  13939  subgmulg  13941  issubg4m  13946  nsgconj  13959  ssnmz  13964  ghmnsgima  14021  subgabl  14085  rdivmuldivd  14389  rhmunitinv  14423  subrguss  14482  subrginv  14483  subrgdv  14484  lsselg  14635  islss3  14653  lspsnel3  14679  lsspropdg  14705  rnglidlmcl  14754  znf1o  14925  topssnei  15153  cnprcl2k  15197  cnss1  15217  cnptopresti  15229  cnptoprest  15230  lmres  15239  txopn  15256  txcnp  15262  xmetres2  15370  blin2  15423  blopn  15481  xmettxlem  15500  xmettx  15501  elcncf2  15565  cncfmet  15583  cncfmptc  15587  cncfmptid  15588  negcncf  15596  mulcncflem  15598  cnrehmeocntop  15601  dedekindeulemuub  15608  dedekindeulemlu  15612  suplociccreex  15615  suplociccex  15616  dedekindicclemuub  15617  dedekindicclemlu  15621  dedekindicclemeu  15622  dedekindicclemicc  15623  ivthinclemlopn  15627  ivthinclemuopn  15629  ivthdec  15635  limcimolemlt  15655  cnplimcim  15658  cnplimclemle  15659  cnplimclemr  15660  cnlimci  15664  limccnpcntop  15666  limccnp2lem  15667  limccnp2cntop  15668  dvlemap  15671  dvfgg  15679  dvidsslem  15684  dvconstss  15689  dvcnp2cntop  15690  dvaddxxbr  15692  dvmulxxbr  15693  dvcoapbr  15698  dvcjbr  15699  plyf  15728  plycolemc  15749  dvply2g  15757  reeff1olem  15762  lgsquadlem3  16078  upgrex  16224  upgr1een  16245  subgruhgredgdm  16391  1hegrvtxdg1fi  16430  wlkvtxiedg  16466  wlkvtxiedgg  16467  sssneq  16902