Theorem sseldd 3249

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   C_ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  disjiun  4125  exmid01  4335  frirrg  4495  ordtri2or2exmid  4718  ontri2orexmidim  4719  riotass  6068  elovimad  6129  funsssuppss  6498  suppssfvg  6503  tfrcldm  6634  nntr2  6776  eroveu  6900  eroprf  6902  ixpssmapg  7010  findcard2d  7195  findcard2sd  7196  fimax2gtrilemstep  7205  elssdc  7209  eqsndc  7210  undifdc  7231  fisseneq  7242  fissfi  7263  fidcenumlemrks  7270  fidcenumlemr  7272  fiuni  7312  suplub2ti  7342  ctssdclemn0  7451  acfun  7564  ccfunen  7631  nnppipi  7711  archnqq  7785  prarloclemlt  7861  suplocexprlemrl  8085  suplocexprlemmu  8086  suplocexprlemdisj  8088  suplocexprlemloc  8089  suplocexprlemex  8090  suplocexprlemub  8091  suplocexprlemlub  8092  suplocsrlemb  8174  suplocsrlempr  8175  suplocsrlem  8176  axpre-suploclemres  8269  suprubex  9284  ind1  9303  suprzclex  9749  infregelbex  10008  fzssp1  10484  elfzoelz  10565  fzofzp1  10656  fzostep1  10667  zssinfcl  10676  suprzubdc  10682  zsupssdc  10684  suprzcl2dc  10685  frecuzrdgg  10868  frecuzrdgdomlem  10869  frecuzrdgsuctlem  10875  ser3mono  10939  seqf1oglem2a  10970  seqf1oglem2  10972  bcm1k  11214  fimaxq  11286  leisorel  11305  zfz1isolemiso  11307  seq3coll  11310  fun2dmnop0  11318  swrdclg  11438  fimaxre2  12010  fiidxsupcl  12012  summodclem2a  12167  fsum3cvg3  12182  fsumcl2lem  12184  fsum0diaglem  12226  fsumiun  12263  prodmodclem2a  12362  fprodcl2lem  12391  fprodap0  12407  fprodrec  12415  fprodap0f  12422  fprodle  12426  bitsfzolem  12740  bitsfzo  12741  uzwodc  12833  4sqlemffi  13198  ballotfilemcdc  13275  ballotfilemsdom  13307  ballotfilemfrceq  13324  ennnfonelemhom  13358  exmidunben  13369  ctiunctlemfo  13382  nninfdclemcl  13391  nninfdclemp1  13393  nninfdclemlt  13394  nninfdclemf1  13395  unbendc  13397  strsetsid  13437  strslssd  13451  gzsumress  13765  resmhm  13847  mhmima  13851  grpidssd  13934  grpinvssd  13935  mulgnnsubcl  13990  mulgnn0subcl  13991  mulgsubcl  13992  mulgpropdg  14020  submmulg  14022  subg0  14036  subgsubcl  14041  subgsub  14042  subgmulg  14044  issubg4m  14049  nsgconj  14062  ssnmz  14067  ghmnsgima  14124  cntzrcl  14153  cntzssv  14154  cntrsubgnsg  14169  cmnsubm  14196  subgabl  14220  rdivmuldivd  14535  rhmunitinv  14569  subrguss  14628  subrginv  14629  subrgdv  14630  lsselg  14782  islss3  14800  ellspsn3  14826  lsspropdg  14852  rnglidlmcl  14901  znf1o  15070  issubassa2  15119  topssnei  15354  cnprcl2k  15398  cnss1  15418  cnptopresti  15430  cnptoprest  15431  lmres  15440  txopn  15457  txcnp  15463  xmetres2  15571  blin2  15624  blopn  15682  xmettxlem  15701  xmettx  15702  elcncf2  15766  cncfmet  15784  cncfmptc  15788  cncfmptid  15789  negcncf  15797  mulcncflem  15799  cnrehmeocntop  15802  dedekindeulemuub  15809  dedekindeulemlu  15813  suplociccreex  15816  suplociccex  15817  dedekindicclemuub  15818  dedekindicclemlu  15822  dedekindicclemeu  15823  dedekindicclemicc  15824  ivthinclemlopn  15828  ivthinclemuopn  15830  ivthdec  15836  limcimolemlt  15856  cnplimcim  15859  cnplimclemle  15860  cnplimclemr  15861  cnlimci  15865  limccnpcntop  15867  limccnp2lem  15868  limccnp2cntop  15869  dvlemap  15872  dvfgg  15880  dvidsslem  15885  dvconstss  15890  dvcnp2cntop  15891  dvaddxxbr  15893  dvmulxxbr  15894  dvcoapbr  15899  dvcjbr  15900  plyf  15929  plycolemc  15950  dvply2g  15958  reeff1olem  15963  lgsquadlem3  16364  upgrex  16510  upgr1een  16531  subgruhgredgdm  16677  1hegrvtxdg1fi  16716  wlkvtxiedg  16752  wlkvtxiedgg  16753  sssneq  17198