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  5662  riotacl  5914  riotasbc  5915  elmpocl  6141  ofrval  6169  f1od2  6321  mpoxopn0yelv  6325  tpostpos  6350  smores  6378  supubti  7101  suplubti  7102  nninfwlporlemd  7274  nninfwlporlem  7275  nninfwlpoimlemg  7277  nninfwlpoimlemginf  7278  prarloclemcalc  7615  rereceu  8002  recriota  8003  rexrd  8122  eqord1  8556  nnred  9049  nncnd  9050  un0addcl  9328  un0mulcl  9329  nnnn0d  9348  nn0red  9349  nn0xnn0d  9367  suprzclex  9471  nn0zd  9493  zred  9495  rpred  9818  ige2m1fz  10232  zsupssdc  10381  zmodfzp1  10493  seq3caopr2  10638  seqf1oglem1  10664  seqf1oglem2  10665  expcl2lemap  10696  m1expcl  10707  ccatrn  11065  summodclem2a  11692  zsumdc  11695  clim2prod  11850  ntrivcvgap  11859  prodmodclem2a  11887  zproddc  11890  bitsfzolem  12265  nninfctlemfo  12361  lcmn0cl  12390  isprm5lem  12463  eulerthlemrprm  12551  eulerthlema  12552  eulerthlemh  12553  eulerthlemth  12554  prmdivdiv  12559  4sqlem13m  12726  4sqlem14  12727  4sqlem17  12730  ennnfonelemg  12774  relelbasov  12894  nmzsubg  13546  conjnmz  13615  conjnmzb  13616  rrgeq0  14027  znf1o  14413  mplelf  14459  mplsubgfilemcl  14461  mplsubgfileminv  14462  mpladd  14466  mplnegfi  14467  lmrcl  14663  lmss  14718  upxp  14744  isxms2  14924  iooretopg  15000  tgqioo  15027  maxcncf  15087  mincncf  15088  ivthreinc  15117  limccoap  15150  dvcl  15155  dvidlemap  15163  dvidrelem  15164  dvidsslem  15165  dvconstss  15170  dvcnp2cntop  15171  plyaddcl  15226  plymulcl  15227  plysubcl  15228  wilthlem1  15452  sgmval2  15456  mpodvdsmulf1o  15462  fsumdvdsmul  15463  sgmmul  15468  perfectlem2  15472  lgscl  15491  lgsquadlem1  15554  lgsquadlem2  15555  2sqlem6  15597  2sqlem8  15600  2sqlem9  15601  2omap  15932  isomninnlem  15969  trilpolemeq1  15979  trilpolemlt1  15980  iswomninnlem  15988  iswomni0  15990  ismkvnnlem  15991  nconstwlpolemgt0  16003