Theorem sselid 3226

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 3224	. 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 3201

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  mptrcl  5738  fnfvimad  5900  riotacl  5997  riotasbc  5998  elmpocl  6227  ofrval  6255  f1od2  6409  elmpom  6412  mpoxopn0yelv  6448  tpostpos  6473  smores  6501  supubti  7241  suplubti  7242  nninfwlporlemd  7414  nninfwlporlem  7415  nninfwlpoimlemg  7417  nninfwlpoimlemginf  7418  prarloclemcalc  7765  rereceu  8152  recriota  8153  rexrd  8272  eqord1  8706  nnred  9199  nncnd  9200  un0addcl  9478  un0mulcl  9479  nnnn0d  9498  nn0red  9499  nn0xnn0d  9517  suprzclex  9621  nn0zd  9643  zred  9645  rpred  9974  ige2m1fz  10388  zsupssdc  10542  zmodfzp1  10654  seq3caopr2  10799  seqf1oglem1  10825  seqf1oglem2  10826  expcl2lemap  10857  m1expcl  10868  ccatrn  11233  wrdind  11350  wrd2ind  11351  summodclem2a  12003  zsumdc  12006  clim2prod  12161  ntrivcvgap  12170  prodmodclem2a  12198  zproddc  12201  bitsfzolem  12576  nninfctlemfo  12672  lcmn0cl  12701  isprm5lem  12774  eulerthlemrprm  12862  eulerthlema  12863  eulerthlemh  12864  eulerthlemth  12865  prmdivdiv  12870  4sqlem13m  13037  4sqlem14  13038  4sqlem17  13041  ennnfonelemg  13085  relelbasov  13206  nmzsubg  13858  conjnmz  13927  conjnmzb  13928  rrgeq0  14341  znf1o  14727  psrbagconf1o  14754  mplelf  14778  mplsubgfilemcl  14780  mplsubgfileminv  14781  mpladd  14785  mplnegfi  14786  lmrcl  14983  lmss  15037  upxp  15063  isxms2  15243  iooretopg  15319  tgqioo  15346  maxcncf  15406  mincncf  15407  ivthreinc  15436  limccoap  15469  dvcl  15474  dvidlemap  15482  dvidrelem  15483  dvidsslem  15484  dvconstss  15489  dvcnp2cntop  15490  plyaddcl  15545  plymulcl  15546  plysubcl  15547  wilthlem1  15771  sgmval2  15775  mpodvdsmulf1o  15781  fsumdvdsmul  15782  sgmmul  15787  perfectlem2  15791  lgscl  15810  lgsquadlem1  15873  lgsquadlem2  15874  2sqlem6  15916  2sqlem8  15919  2sqlem9  15920  upgrss  16017  usgrss  16095  wlkres  16297  trlreslem  16307  2omap  16692  isomninnlem  16739  trilpolemeq1  16749  trilpolemlt1  16750  iswomninnlem  16759  iswomni0  16761  ismkvnnlem  16762  nconstwlpolemgt0  16774