Theorem sselid 3225

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

Syntax hints:   -> wi 4   e. wcel 2202   C_ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  mptrcl  5729  fnfvimad  5890  riotacl  5987  riotasbc  5988  elmpocl  6217  ofrval  6246  f1od2  6400  elmpom  6403  mpoxopn0yelv  6405  tpostpos  6430  smores  6458  supubti  7198  suplubti  7199  nninfwlporlemd  7371  nninfwlporlem  7372  nninfwlpoimlemg  7374  nninfwlpoimlemginf  7375  prarloclemcalc  7722  rereceu  8109  recriota  8110  rexrd  8229  eqord1  8663  nnred  9156  nncnd  9157  un0addcl  9435  un0mulcl  9436  nnnn0d  9455  nn0red  9456  nn0xnn0d  9474  suprzclex  9578  nn0zd  9600  zred  9602  rpred  9931  ige2m1fz  10345  zsupssdc  10499  zmodfzp1  10611  seq3caopr2  10756  seqf1oglem1  10782  seqf1oglem2  10783  expcl2lemap  10814  m1expcl  10825  ccatrn  11190  wrdind  11307  wrd2ind  11308  summodclem2a  11960  zsumdc  11963  clim2prod  12118  ntrivcvgap  12127  prodmodclem2a  12155  zproddc  12158  bitsfzolem  12533  nninfctlemfo  12629  lcmn0cl  12658  isprm5lem  12731  eulerthlemrprm  12819  eulerthlema  12820  eulerthlemh  12821  eulerthlemth  12822  prmdivdiv  12827  4sqlem13m  12994  4sqlem14  12995  4sqlem17  12998  ennnfonelemg  13042  relelbasov  13163  nmzsubg  13815  conjnmz  13884  conjnmzb  13885  rrgeq0  14298  znf1o  14684  mplelf  14730  mplsubgfilemcl  14732  mplsubgfileminv  14733  mpladd  14737  mplnegfi  14738  lmrcl  14935  lmss  14989  upxp  15015  isxms2  15195  iooretopg  15271  tgqioo  15298  maxcncf  15358  mincncf  15359  ivthreinc  15388  limccoap  15421  dvcl  15426  dvidlemap  15434  dvidrelem  15435  dvidsslem  15436  dvconstss  15441  dvcnp2cntop  15442  plyaddcl  15497  plymulcl  15498  plysubcl  15499  wilthlem1  15723  sgmval2  15727  mpodvdsmulf1o  15733  fsumdvdsmul  15734  sgmmul  15739  perfectlem2  15743  lgscl  15762  lgsquadlem1  15825  lgsquadlem2  15826  2sqlem6  15868  2sqlem8  15871  2sqlem9  15872  upgrss  15969  usgrss  16047  wlkres  16249  trlreslem  16259  2omap  16645  isomninnlem  16685  trilpolemeq1  16695  trilpolemlt1  16696  iswomninnlem  16705  iswomni0  16707  ismkvnnlem  16708  nconstwlpolemgt0  16720