Theorem sselid 3182

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

Syntax hints:   -> wi 4   e. wcel 2167   C_ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  mptrcl  5645  riotacl  5893  riotasbc  5894  elmpocl  6120  ofrval  6148  f1od2  6295  mpoxopn0yelv  6299  tpostpos  6324  smores  6352  supubti  7067  suplubti  7068  nninfwlporlemd  7240  nninfwlporlem  7241  nninfwlpoimlemg  7243  nninfwlpoimlemginf  7244  prarloclemcalc  7572  rereceu  7959  recriota  7960  rexrd  8079  eqord1  8513  nnred  9006  nncnd  9007  un0addcl  9285  un0mulcl  9286  nnnn0d  9305  nn0red  9306  nn0xnn0d  9324  suprzclex  9427  nn0zd  9449  zred  9451  rpred  9774  ige2m1fz  10188  zsupssdc  10331  zmodfzp1  10443  seq3caopr2  10588  seqf1oglem1  10614  seqf1oglem2  10615  expcl2lemap  10646  m1expcl  10657  summodclem2a  11549  zsumdc  11552  clim2prod  11707  ntrivcvgap  11716  prodmodclem2a  11744  zproddc  11747  bitsfzolem  12122  nninfctlemfo  12218  lcmn0cl  12247  isprm5lem  12320  eulerthlemrprm  12408  eulerthlema  12409  eulerthlemh  12410  eulerthlemth  12411  prmdivdiv  12416  4sqlem13m  12583  4sqlem14  12584  4sqlem17  12587  ennnfonelemg  12631  relelbasov  12751  nmzsubg  13366  conjnmz  13435  conjnmzb  13436  rrgeq0  13847  znf1o  14233  lmrcl  14453  lmss  14508  upxp  14534  isxms2  14714  iooretopg  14790  tgqioo  14817  maxcncf  14877  mincncf  14878  ivthreinc  14907  limccoap  14940  dvcl  14945  dvidlemap  14953  dvidrelem  14954  dvidsslem  14955  dvconstss  14960  dvcnp2cntop  14961  plyaddcl  15016  plymulcl  15017  plysubcl  15018  wilthlem1  15242  sgmval2  15246  mpodvdsmulf1o  15252  fsumdvdsmul  15253  sgmmul  15258  perfectlem2  15262  lgscl  15281  lgsquadlem1  15344  lgsquadlem2  15345  2sqlem6  15387  2sqlem8  15390  2sqlem9  15391  isomninnlem  15701  trilpolemeq1  15711  trilpolemlt1  15712  iswomninnlem  15720  iswomni0  15722  ismkvnnlem  15723  nconstwlpolemgt0  15735