Theorem sselid 3168

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

Syntax hints:   -> wi 4   e. wcel 2160   C_ wss 3144

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-in 3150  df-ss 3157

This theorem is referenced by:  mptrcl  5619  riotacl  5866  riotasbc  5867  elmpocl  6091  ofrval  6117  f1od2  6260  mpoxopn0yelv  6264  tpostpos  6289  smores  6317  supubti  7028  suplubti  7029  nninfwlporlemd  7200  nninfwlporlem  7201  nninfwlpoimlemg  7203  nninfwlpoimlemginf  7204  prarloclemcalc  7531  rereceu  7918  recriota  7919  rexrd  8037  eqord1  8470  nnred  8962  nncnd  8963  un0addcl  9239  un0mulcl  9240  nnnn0d  9259  nn0red  9260  nn0xnn0d  9278  suprzclex  9381  nn0zd  9403  zred  9405  rpred  9726  ige2m1fz  10140  zmodfzp1  10379  seq3caopr2  10513  expcl2lemap  10563  m1expcl  10574  summodclem2a  11421  zsumdc  11424  clim2prod  11579  ntrivcvgap  11588  prodmodclem2a  11616  zproddc  11619  zsupssdc  11987  lcmn0cl  12100  isprm5lem  12173  eulerthlemrprm  12261  eulerthlema  12262  eulerthlemh  12263  eulerthlemth  12264  prmdivdiv  12269  4sqlem13m  12435  4sqlem14  12436  4sqlem17  12439  ennnfonelemg  12454  relelbasov  12574  nmzsubg  13149  conjnmz  13218  conjnmzb  13219  lmrcl  14148  lmss  14203  upxp  14229  isxms2  14409  iooretopg  14485  tgqioo  14504  limccoap  14604  dvcl  14609  dvidlemap  14617  dvcnp2cntop  14620  wilthlem1  14855  lgscl  14873  2sqlem6  14925  2sqlem8  14928  2sqlem9  14929  isomninnlem  15237  trilpolemeq1  15247  trilpolemlt1  15248  iswomninnlem  15256  iswomni0  15258  ismkvnnlem  15259  nconstwlpolemgt0  15271