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  4337  frirrg  4497  ordtri2or2exmid  4720  ontri2orexmidim  4721  riotass  6071  elovimad  6132  funsssuppss  6502  suppssfvg  6507  tfrcldm  6638  nntr2  6780  eroveu  6904  eroprf  6906  ixpssmapg  7014  findcard2d  7199  findcard2sd  7200  fimax2gtrilemstep  7209  elssdc  7213  eqsndc  7214  undifdc  7235  fisseneq  7246  fissfi  7267  fidcenumlemrks  7275  fidcenumlemr  7277  fiuni  7317  suplub2ti  7347  ctssdclemn0  7456  acfun  7569  ccfunen  7636  nnppipi  7716  archnqq  7790  prarloclemlt  7866  suplocexprlemrl  8090  suplocexprlemmu  8091  suplocexprlemdisj  8093  suplocexprlemloc  8094  suplocexprlemex  8095  suplocexprlemub  8096  suplocexprlemlub  8097  suplocsrlemb  8179  suplocsrlempr  8180  suplocsrlem  8181  axpre-suploclemres  8274  suprubex  9289  ind1  9309  suprzclex  9755  infregelbex  10014  fzssp1  10490  elfzoelz  10571  fzofzp1  10662  fzostep1  10673  zssinfcl  10682  suprzubdc  10688  zsupssdc  10690  suprzcl2dc  10691  frecuzrdgg  10874  frecuzrdgdomlem  10875  frecuzrdgsuctlem  10881  ser3mono  10945  seqf1oglem2a  10976  seqf1oglem2  10978  bcm1k  11220  fimaxq  11292  leisorel  11311  zfz1isolemiso  11313  seq3coll  11316  fun2dmnop0  11324  swrdclg  11444  fimaxre2  12016  fiidxsupcl  12018  summodclem2a  12173  fsum3cvg3  12188  fsumcl2lem  12190  fsum0diaglem  12232  fsumiun  12269  prodmodclem2a  12368  fprodcl2lem  12397  fprodap0  12413  fprodrec  12421  fprodap0f  12428  fprodle  12432  bitsfzolem  12746  bitsfzo  12747  uzwodc  12839  4sqlemffi  13204  ballotfilemcdc  13281  ballotfilemsdom  13313  ballotfilemfrceq  13330  ennnfonelemhom  13364  exmidunben  13375  ctiunctlemfo  13388  nninfdclemcl  13397  nninfdclemp1  13399  nninfdclemlt  13400  nninfdclemf1  13401  unbendc  13403  strsetsid  13443  strslssd  13457  gzsumress  13771  resmhm  13853  mhmima  13857  grpidssd  13940  grpinvssd  13941  mulgnnsubcl  13996  mulgnn0subcl  13997  mulgsubcl  13998  mulgpropdg  14026  submmulg  14028  subg0  14042  subgsubcl  14047  subgsub  14048  subgmulg  14050  issubg4m  14055  nsgconj  14068  ssnmz  14073  ghmnsgima  14130  cntzrcl  14159  cntzssv  14160  cntrsubgnsg  14175  cmnsubm  14202  subgabl  14226  gsummptfidmsplit  14254  rdivmuldivd  14560  rhmunitinv  14594  subrguss  14653  subrginv  14654  subrgdv  14655  lsselg  14807  islss3  14825  ellspsn3  14851  lsspropdg  14877  rnglidlmcl  14926  znf1o  15095  issubassa2  15144  topssnei  15388  cnprcl2k  15432  cnss1  15452  cnptopresti  15464  cnptoprest  15465  lmres  15474  txopn  15491  txcnp  15497  xmetres2  15605  blin2  15658  blopn  15716  xmettxlem  15735  xmettx  15736  elcncf2  15800  cncfmet  15818  cncfmptc  15822  cncfmptid  15823  negcncf  15831  mulcncflem  15833  cnrehmeocntop  15836  dedekindeulemuub  15843  dedekindeulemlu  15847  suplociccreex  15850  suplociccex  15851  dedekindicclemuub  15852  dedekindicclemlu  15856  dedekindicclemeu  15857  dedekindicclemicc  15858  ivthinclemlopn  15862  ivthinclemuopn  15864  ivthdec  15870  limcimolemlt  15890  cnplimcim  15893  cnplimclemle  15894  cnplimclemr  15895  cnlimci  15899  limccnpcntop  15901  limccnp2lem  15902  limccnp2cntop  15903  dvlemap  15906  dvfgg  15914  dvidsslem  15919  dvconstss  15924  dvcnp2cntop  15925  dvaddxxbr  15927  dvmulxxbr  15928  dvcoapbr  15933  dvcjbr  15934  plyf  15963  plycolemc  15984  dvply2g  15992  reeff1olem  15997  lgsquadlem3  16403  upgrex  16549  upgr1een  16570  subgruhgredgdm  16716  1hegrvtxdg1fi  16755  wlkvtxiedg  16791  wlkvtxiedgg  16792  sssneq  17237