Theorem sseldd 3225

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

Syntax hints:   -> wi 4   e. wcel 2200   C_ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  disjiun  4078  exmid01  4282  frirrg  4441  ordtri2or2exmid  4663  ontri2orexmidim  4664  riotass  5984  elovimad  6045  tfrcldm  6509  nntr2  6649  eroveu  6773  eroprf  6775  ixpssmapg  6875  findcard2d  7053  findcard2sd  7054  fimax2gtrilemstep  7062  undifdc  7086  fisseneq  7096  fidcenumlemrks  7120  fidcenumlemr  7122  fiuni  7145  suplub2ti  7168  ctssdclemn0  7277  acfun  7389  ccfunen  7450  nnppipi  7530  archnqq  7604  prarloclemlt  7680  suplocexprlemrl  7904  suplocexprlemmu  7905  suplocexprlemdisj  7907  suplocexprlemloc  7908  suplocexprlemex  7909  suplocexprlemub  7910  suplocexprlemlub  7911  suplocsrlemb  7993  suplocsrlempr  7994  suplocsrlem  7995  axpre-suploclemres  8088  suprubex  9098  suprzclex  9545  infregelbex  9793  fzssp1  10263  elfzoelz  10343  fzofzp1  10433  fzostep1  10443  zssinfcl  10452  suprzubdc  10456  zsupssdc  10458  suprzcl2dc  10459  frecuzrdgg  10638  frecuzrdgdomlem  10639  frecuzrdgsuctlem  10645  ser3mono  10709  seqf1oglem2a  10740  seqf1oglem2  10742  bcm1k  10982  fimaxq  11049  leisorel  11059  zfz1isolemiso  11061  seq3coll  11064  fun2dmnop0  11069  swrdclg  11182  fimaxre2  11738  summodclem2a  11892  fsum3cvg3  11907  fsumcl2lem  11909  fsum0diaglem  11951  fsumiun  11988  prodmodclem2a  12087  fprodcl2lem  12116  fprodap0  12132  fprodrec  12140  fprodap0f  12147  fprodle  12151  bitsfzolem  12465  bitsfzo  12466  uzwodc  12558  4sqlemffi  12919  ennnfonelemhom  12986  exmidunben  12997  ctiunctlemfo  13010  nninfdclemcl  13019  nninfdclemp1  13021  nninfdclemlt  13022  nninfdclemf1  13023  unbendc  13025  strsetsid  13065  strslssd  13079  gsumpropd2  13426  gsumress  13428  resmhm  13520  mhmima  13524  grpidssd  13609  grpinvssd  13610  mulgnnsubcl  13671  mulgnn0subcl  13672  mulgsubcl  13673  mulgpropdg  13701  submmulg  13703  subg0  13717  subgsubcl  13722  subgsub  13723  subgmulg  13725  issubg4m  13730  nsgconj  13743  ssnmz  13748  ghmnsgima  13805  subgabl  13869  rdivmuldivd  14108  rhmunitinv  14142  subrguss  14200  subrginv  14201  subrgdv  14202  lsselg  14325  islss3  14343  lspsnel3  14369  lsspropdg  14395  rnglidlmcl  14444  znf1o  14615  topssnei  14836  cnprcl2k  14880  cnss1  14900  cnptopresti  14912  cnptoprest  14913  lmres  14922  txopn  14939  txcnp  14945  xmetres2  15053  blin2  15106  blopn  15164  xmettxlem  15183  xmettx  15184  elcncf2  15248  cncfmet  15266  cncfmptc  15270  cncfmptid  15271  negcncf  15279  mulcncflem  15281  cnrehmeocntop  15284  dedekindeulemuub  15291  dedekindeulemlu  15295  suplociccreex  15298  suplociccex  15299  dedekindicclemuub  15300  dedekindicclemlu  15304  dedekindicclemeu  15305  dedekindicclemicc  15306  ivthinclemlopn  15310  ivthinclemuopn  15312  ivthdec  15318  limcimolemlt  15338  cnplimcim  15341  cnplimclemle  15342  cnplimclemr  15343  cnlimci  15347  limccnpcntop  15349  limccnp2lem  15350  limccnp2cntop  15351  dvlemap  15354  dvfgg  15362  dvidsslem  15367  dvconstss  15372  dvcnp2cntop  15373  dvaddxxbr  15375  dvmulxxbr  15376  dvcoapbr  15381  dvcjbr  15382  plyf  15411  plycolemc  15432  dvply2g  15440  reeff1olem  15445  lgsquadlem3  15758  upgrex  15903  wlkvtxiedg  16056  wlkvtxiedgg  16057  sssneq  16368