Theorem sselid 3177

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

Syntax hints:   -> wi 4   e. wcel 2164   C_ wss 3153

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 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3159  df-ss 3166

This theorem is referenced by:  mptrcl  5640  riotacl  5888  riotasbc  5889  elmpocl  6113  ofrval  6141  f1od2  6288  mpoxopn0yelv  6292  tpostpos  6317  smores  6345  supubti  7058  suplubti  7059  nninfwlporlemd  7231  nninfwlporlem  7232  nninfwlpoimlemg  7234  nninfwlpoimlemginf  7235  prarloclemcalc  7562  rereceu  7949  recriota  7950  rexrd  8069  eqord1  8502  nnred  8995  nncnd  8996  un0addcl  9273  un0mulcl  9274  nnnn0d  9293  nn0red  9294  nn0xnn0d  9312  suprzclex  9415  nn0zd  9437  zred  9439  rpred  9762  ige2m1fz  10176  zmodfzp1  10419  seq3caopr2  10564  seqf1oglem1  10590  seqf1oglem2  10591  expcl2lemap  10622  m1expcl  10633  summodclem2a  11524  zsumdc  11527  clim2prod  11682  ntrivcvgap  11691  prodmodclem2a  11719  zproddc  11722  zsupssdc  12091  nninfctlemfo  12177  lcmn0cl  12206  isprm5lem  12279  eulerthlemrprm  12367  eulerthlema  12368  eulerthlemh  12369  eulerthlemth  12370  prmdivdiv  12375  4sqlem13m  12541  4sqlem14  12542  4sqlem17  12545  ennnfonelemg  12560  relelbasov  12680  nmzsubg  13280  conjnmz  13349  conjnmzb  13350  rrgeq0  13761  znf1o  14139  lmrcl  14359  lmss  14414  upxp  14440  isxms2  14620  iooretopg  14696  tgqioo  14715  maxcncf  14769  mincncf  14770  ivthreinc  14799  limccoap  14832  dvcl  14837  dvidlemap  14845  dvcnp2cntop  14848  plyaddcl  14900  plymulcl  14901  plysubcl  14902  wilthlem1  15112  lgscl  15130  lgsquadlem1  15191  2sqlem6  15207  2sqlem8  15210  2sqlem9  15211  isomninnlem  15520  trilpolemeq1  15530  trilpolemlt1  15531  iswomninnlem  15539  iswomni0  15541  ismkvnnlem  15542  nconstwlpolemgt0  15554