Theorem sselid 3199

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 3197	. 2 |- ( C e. A -> C e. B )
4	1, 3	syl 14	1 |- ( ph -> C e. B )

Syntax hints:   -> wi 4   e. wcel 2178   C_ wss 3174

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-in 3180  df-ss 3187

This theorem is referenced by:  mptrcl  5685  riotacl  5937  riotasbc  5938  elmpocl  6164  ofrval  6192  f1od2  6344  mpoxopn0yelv  6348  tpostpos  6373  smores  6401  supubti  7127  suplubti  7128  nninfwlporlemd  7300  nninfwlporlem  7301  nninfwlpoimlemg  7303  nninfwlpoimlemginf  7304  prarloclemcalc  7650  rereceu  8037  recriota  8038  rexrd  8157  eqord1  8591  nnred  9084  nncnd  9085  un0addcl  9363  un0mulcl  9364  nnnn0d  9383  nn0red  9384  nn0xnn0d  9402  suprzclex  9506  nn0zd  9528  zred  9530  rpred  9853  ige2m1fz  10267  zsupssdc  10418  zmodfzp1  10530  seq3caopr2  10675  seqf1oglem1  10701  seqf1oglem2  10702  expcl2lemap  10733  m1expcl  10744  ccatrn  11103  wrdind  11213  wrd2ind  11214  summodclem2a  11807  zsumdc  11810  clim2prod  11965  ntrivcvgap  11974  prodmodclem2a  12002  zproddc  12005  bitsfzolem  12380  nninfctlemfo  12476  lcmn0cl  12505  isprm5lem  12578  eulerthlemrprm  12666  eulerthlema  12667  eulerthlemh  12668  eulerthlemth  12669  prmdivdiv  12674  4sqlem13m  12841  4sqlem14  12842  4sqlem17  12845  ennnfonelemg  12889  relelbasov  13009  nmzsubg  13661  conjnmz  13730  conjnmzb  13731  rrgeq0  14142  znf1o  14528  mplelf  14574  mplsubgfilemcl  14576  mplsubgfileminv  14577  mpladd  14581  mplnegfi  14582  lmrcl  14778  lmss  14833  upxp  14859  isxms2  15039  iooretopg  15115  tgqioo  15142  maxcncf  15202  mincncf  15203  ivthreinc  15232  limccoap  15265  dvcl  15270  dvidlemap  15278  dvidrelem  15279  dvidsslem  15280  dvconstss  15285  dvcnp2cntop  15286  plyaddcl  15341  plymulcl  15342  plysubcl  15343  wilthlem1  15567  sgmval2  15571  mpodvdsmulf1o  15577  fsumdvdsmul  15578  sgmmul  15583  perfectlem2  15587  lgscl  15606  lgsquadlem1  15669  lgsquadlem2  15670  2sqlem6  15712  2sqlem8  15715  2sqlem9  15716  upgrss  15810  2omap  16132  isomninnlem  16171  trilpolemeq1  16181  trilpolemlt1  16182  iswomninnlem  16190  iswomni0  16192  ismkvnnlem  16193  nconstwlpolemgt0  16205