Theorem sselid 3222

Description: Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.)

Hypotheses

Ref	Expression
sseli.1	|- A C_ B
sselid.2	|- ( ph -> C e. A )

Assertion

Ref	Expression
sselid	|- ( ph -> C e. B )

Proof of Theorem sselid

Step	Hyp	Ref	Expression
1		sselid.2	. 2 |- ( ph -> C e. A )
2		sseli.1	. . 3 |- A C_ B
3	2	sseli 3220	. 2 |- ( C e. A -> C e. B )
4	1, 3	syl 14	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:  mptrcl  5717  riotacl  5970  riotasbc  5971  elmpocl  6200  ofrval  6229  f1od2  6381  mpoxopn0yelv  6385  tpostpos  6410  smores  6438  supubti  7166  suplubti  7167  nninfwlporlemd  7339  nninfwlporlem  7340  nninfwlpoimlemg  7342  nninfwlpoimlemginf  7343  prarloclemcalc  7689  rereceu  8076  recriota  8077  rexrd  8196  eqord1  8630  nnred  9123  nncnd  9124  un0addcl  9402  un0mulcl  9403  nnnn0d  9422  nn0red  9423  nn0xnn0d  9441  suprzclex  9545  nn0zd  9567  zred  9569  rpred  9892  ige2m1fz  10306  zsupssdc  10458  zmodfzp1  10570  seq3caopr2  10715  seqf1oglem1  10741  seqf1oglem2  10742  expcl2lemap  10773  m1expcl  10784  ccatrn  11144  wrdind  11254  wrd2ind  11255  summodclem2a  11892  zsumdc  11895  clim2prod  12050  ntrivcvgap  12059  prodmodclem2a  12087  zproddc  12090  bitsfzolem  12465  nninfctlemfo  12561  lcmn0cl  12590  isprm5lem  12663  eulerthlemrprm  12751  eulerthlema  12752  eulerthlemh  12753  eulerthlemth  12754  prmdivdiv  12759  4sqlem13m  12926  4sqlem14  12927  4sqlem17  12930  ennnfonelemg  12974  relelbasov  13095  nmzsubg  13747  conjnmz  13816  conjnmzb  13817  rrgeq0  14229  znf1o  14615  mplelf  14661  mplsubgfilemcl  14663  mplsubgfileminv  14664  mpladd  14668  mplnegfi  14669  lmrcl  14866  lmss  14920  upxp  14946  isxms2  15126  iooretopg  15202  tgqioo  15229  maxcncf  15289  mincncf  15290  ivthreinc  15319  limccoap  15352  dvcl  15357  dvidlemap  15365  dvidrelem  15366  dvidsslem  15367  dvconstss  15372  dvcnp2cntop  15373  plyaddcl  15428  plymulcl  15429  plysubcl  15430  wilthlem1  15654  sgmval2  15658  mpodvdsmulf1o  15664  fsumdvdsmul  15665  sgmmul  15670  perfectlem2  15674  lgscl  15693  lgsquadlem1  15756  lgsquadlem2  15757  2sqlem6  15799  2sqlem8  15802  2sqlem9  15803  upgrss  15899  usgrss  15975  2omap  16359  isomninnlem  16398  trilpolemeq1  16408  trilpolemlt1  16409  iswomninnlem  16417  iswomni0  16419  ismkvnnlem  16420  nconstwlpolemgt0  16432