Theorem sseldd 3229

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

Syntax hints:   -> wi 4   e. wcel 2202   C_ wss 3201

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 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  disjiun  4088  exmid01  4294  frirrg  4453  ordtri2or2exmid  4675  ontri2orexmidim  4676  riotass  6011  elovimad  6072  funsssuppss  6436  suppssfvg  6441  tfrcldm  6572  nntr2  6714  eroveu  6838  eroprf  6840  ixpssmapg  6940  findcard2d  7123  findcard2sd  7124  fimax2gtrilemstep  7133  elssdc  7137  eqsndc  7138  undifdc  7159  fisseneq  7170  fidcenumlemrks  7195  fidcenumlemr  7197  fiuni  7220  suplub2ti  7243  ctssdclemn0  7352  acfun  7465  ccfunen  7526  nnppipi  7606  archnqq  7680  prarloclemlt  7756  suplocexprlemrl  7980  suplocexprlemmu  7981  suplocexprlemdisj  7983  suplocexprlemloc  7984  suplocexprlemex  7985  suplocexprlemub  7986  suplocexprlemlub  7987  suplocsrlemb  8069  suplocsrlempr  8070  suplocsrlem  8071  axpre-suploclemres  8164  suprubex  9173  suprzclex  9622  infregelbex  9876  fzssp1  10347  elfzoelz  10427  fzofzp1  10518  fzostep1  10529  zssinfcl  10538  suprzubdc  10542  zsupssdc  10544  suprzcl2dc  10545  frecuzrdgg  10724  frecuzrdgdomlem  10725  frecuzrdgsuctlem  10731  ser3mono  10795  seqf1oglem2a  10826  seqf1oglem2  10828  bcm1k  11068  fimaxq  11137  leisorel  11147  zfz1isolemiso  11149  seq3coll  11152  fun2dmnop0  11160  swrdclg  11280  fimaxre2  11850  summodclem2a  12005  fsum3cvg3  12020  fsumcl2lem  12022  fsum0diaglem  12064  fsumiun  12101  prodmodclem2a  12200  fprodcl2lem  12229  fprodap0  12245  fprodrec  12253  fprodap0f  12260  fprodle  12264  bitsfzolem  12578  bitsfzo  12579  uzwodc  12671  4sqlemffi  13032  ennnfonelemhom  13099  exmidunben  13110  ctiunctlemfo  13123  nninfdclemcl  13132  nninfdclemp1  13134  nninfdclemlt  13135  nninfdclemf1  13136  unbendc  13138  strsetsid  13178  strslssd  13192  gsumpropd2  13539  gsumress  13541  resmhm  13633  mhmima  13637  grpidssd  13722  grpinvssd  13723  mulgnnsubcl  13784  mulgnn0subcl  13785  mulgsubcl  13786  mulgpropdg  13814  submmulg  13816  subg0  13830  subgsubcl  13835  subgsub  13836  subgmulg  13838  issubg4m  13843  nsgconj  13856  ssnmz  13861  ghmnsgima  13918  subgabl  13982  rdivmuldivd  14222  rhmunitinv  14256  subrguss  14314  subrginv  14315  subrgdv  14316  lsselg  14440  islss3  14458  lspsnel3  14484  lsspropdg  14510  rnglidlmcl  14559  znf1o  14730  topssnei  14956  cnprcl2k  15000  cnss1  15020  cnptopresti  15032  cnptoprest  15033  lmres  15042  txopn  15059  txcnp  15065  xmetres2  15173  blin2  15226  blopn  15284  xmettxlem  15303  xmettx  15304  elcncf2  15368  cncfmet  15386  cncfmptc  15390  cncfmptid  15391  negcncf  15399  mulcncflem  15401  cnrehmeocntop  15404  dedekindeulemuub  15411  dedekindeulemlu  15415  suplociccreex  15418  suplociccex  15419  dedekindicclemuub  15420  dedekindicclemlu  15424  dedekindicclemeu  15425  dedekindicclemicc  15426  ivthinclemlopn  15430  ivthinclemuopn  15432  ivthdec  15438  limcimolemlt  15458  cnplimcim  15461  cnplimclemle  15462  cnplimclemr  15463  cnlimci  15467  limccnpcntop  15469  limccnp2lem  15470  limccnp2cntop  15471  dvlemap  15474  dvfgg  15482  dvidsslem  15487  dvconstss  15492  dvcnp2cntop  15493  dvaddxxbr  15495  dvmulxxbr  15496  dvcoapbr  15501  dvcjbr  15502  plyf  15531  plycolemc  15552  dvply2g  15560  reeff1olem  15565  lgsquadlem3  15881  upgrex  16027  upgr1een  16048  subgruhgredgdm  16194  1hegrvtxdg1fi  16233  wlkvtxiedg  16269  wlkvtxiedgg  16270  sssneq  16707