Theorem sselid 3191

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

Syntax hints:   -> wi 4   e. wcel 2176   C_ wss 3166

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179

This theorem is referenced by:  mptrcl  5664  riotacl  5916  riotasbc  5917  elmpocl  6143  ofrval  6171  f1od2  6323  mpoxopn0yelv  6327  tpostpos  6352  smores  6380  supubti  7103  suplubti  7104  nninfwlporlemd  7276  nninfwlporlem  7277  nninfwlpoimlemg  7279  nninfwlpoimlemginf  7280  prarloclemcalc  7617  rereceu  8004  recriota  8005  rexrd  8124  eqord1  8558  nnred  9051  nncnd  9052  un0addcl  9330  un0mulcl  9331  nnnn0d  9350  nn0red  9351  nn0xnn0d  9369  suprzclex  9473  nn0zd  9495  zred  9497  rpred  9820  ige2m1fz  10234  zsupssdc  10383  zmodfzp1  10495  seq3caopr2  10640  seqf1oglem1  10666  seqf1oglem2  10667  expcl2lemap  10698  m1expcl  10709  ccatrn  11068  summodclem2a  11725  zsumdc  11728  clim2prod  11883  ntrivcvgap  11892  prodmodclem2a  11920  zproddc  11923  bitsfzolem  12298  nninfctlemfo  12394  lcmn0cl  12423  isprm5lem  12496  eulerthlemrprm  12584  eulerthlema  12585  eulerthlemh  12586  eulerthlemth  12587  prmdivdiv  12592  4sqlem13m  12759  4sqlem14  12760  4sqlem17  12763  ennnfonelemg  12807  relelbasov  12927  nmzsubg  13579  conjnmz  13648  conjnmzb  13649  rrgeq0  14060  znf1o  14446  mplelf  14492  mplsubgfilemcl  14494  mplsubgfileminv  14495  mpladd  14499  mplnegfi  14500  lmrcl  14696  lmss  14751  upxp  14777  isxms2  14957  iooretopg  15033  tgqioo  15060  maxcncf  15120  mincncf  15121  ivthreinc  15150  limccoap  15183  dvcl  15188  dvidlemap  15196  dvidrelem  15197  dvidsslem  15198  dvconstss  15203  dvcnp2cntop  15204  plyaddcl  15259  plymulcl  15260  plysubcl  15261  wilthlem1  15485  sgmval2  15489  mpodvdsmulf1o  15495  fsumdvdsmul  15496  sgmmul  15501  perfectlem2  15505  lgscl  15524  lgsquadlem1  15587  lgsquadlem2  15588  2sqlem6  15630  2sqlem8  15633  2sqlem9  15634  2omap  15969  isomninnlem  16006  trilpolemeq1  16016  trilpolemlt1  16017  iswomninnlem  16025  iswomni0  16027  ismkvnnlem  16028  nconstwlpolemgt0  16040