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  4077  exmid01  4281  frirrg  4440  ordtri2or2exmid  4662  ontri2orexmidim  4663  riotass  5983  elovimad  6044  tfrcldm  6507  nntr2  6647  eroveu  6771  eroprf  6773  ixpssmapg  6873  findcard2d  7049  findcard2sd  7050  fimax2gtrilemstep  7058  undifdc  7082  fisseneq  7092  fidcenumlemrks  7116  fidcenumlemr  7118  fiuni  7141  suplub2ti  7164  ctssdclemn0  7273  acfun  7385  ccfunen  7446  nnppipi  7526  archnqq  7600  prarloclemlt  7676  suplocexprlemrl  7900  suplocexprlemmu  7901  suplocexprlemdisj  7903  suplocexprlemloc  7904  suplocexprlemex  7905  suplocexprlemub  7906  suplocexprlemlub  7907  suplocsrlemb  7989  suplocsrlempr  7990  suplocsrlem  7991  axpre-suploclemres  8084  suprubex  9094  suprzclex  9541  infregelbex  9789  fzssp1  10259  elfzoelz  10339  fzofzp1  10428  fzostep1  10438  zssinfcl  10447  suprzubdc  10451  zsupssdc  10453  suprzcl2dc  10454  frecuzrdgg  10633  frecuzrdgdomlem  10634  frecuzrdgsuctlem  10640  ser3mono  10704  seqf1oglem2a  10735  seqf1oglem2  10737  bcm1k  10977  fimaxq  11044  leisorel  11054  zfz1isolemiso  11056  seq3coll  11059  fun2dmnop0  11064  swrdclg  11177  fimaxre2  11733  summodclem2a  11887  fsum3cvg3  11902  fsumcl2lem  11904  fsum0diaglem  11946  fsumiun  11983  prodmodclem2a  12082  fprodcl2lem  12111  fprodap0  12127  fprodrec  12135  fprodap0f  12142  fprodle  12146  bitsfzolem  12460  bitsfzo  12461  uzwodc  12553  4sqlemffi  12914  ennnfonelemhom  12981  exmidunben  12992  ctiunctlemfo  13005  nninfdclemcl  13014  nninfdclemp1  13016  nninfdclemlt  13017  nninfdclemf1  13018  unbendc  13020  strsetsid  13060  strslssd  13074  gsumpropd2  13421  gsumress  13423  resmhm  13515  mhmima  13519  grpidssd  13604  grpinvssd  13605  mulgnnsubcl  13666  mulgnn0subcl  13667  mulgsubcl  13668  mulgpropdg  13696  submmulg  13698  subg0  13712  subgsubcl  13717  subgsub  13718  subgmulg  13720  issubg4m  13725  nsgconj  13738  ssnmz  13743  ghmnsgima  13800  subgabl  13864  rdivmuldivd  14102  rhmunitinv  14136  subrguss  14194  subrginv  14195  subrgdv  14196  lsselg  14319  islss3  14337  lspsnel3  14363  lsspropdg  14389  rnglidlmcl  14438  znf1o  14609  topssnei  14830  cnprcl2k  14874  cnss1  14894  cnptopresti  14906  cnptoprest  14907  lmres  14916  txopn  14933  txcnp  14939  xmetres2  15047  blin2  15100  blopn  15158  xmettxlem  15177  xmettx  15178  elcncf2  15242  cncfmet  15260  cncfmptc  15264  cncfmptid  15265  negcncf  15273  mulcncflem  15275  cnrehmeocntop  15278  dedekindeulemuub  15285  dedekindeulemlu  15289  suplociccreex  15292  suplociccex  15293  dedekindicclemuub  15294  dedekindicclemlu  15298  dedekindicclemeu  15299  dedekindicclemicc  15300  ivthinclemlopn  15304  ivthinclemuopn  15306  ivthdec  15312  limcimolemlt  15332  cnplimcim  15335  cnplimclemle  15336  cnplimclemr  15337  cnlimci  15341  limccnpcntop  15343  limccnp2lem  15344  limccnp2cntop  15345  dvlemap  15348  dvfgg  15356  dvidsslem  15361  dvconstss  15366  dvcnp2cntop  15367  dvaddxxbr  15369  dvmulxxbr  15370  dvcoapbr  15375  dvcjbr  15376  plyf  15405  plycolemc  15426  dvply2g  15434  reeff1olem  15439  lgsquadlem3  15752  upgrex  15897  wlkvtxiedgg  16042  sssneq  16327