Theorem sseldi 3059

Description: Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.)

Hypotheses

Ref	Expression
sseli.1	|- A C_ B
sseldi.2	|- ( ph -> C e. A )

Assertion

Ref	Expression
sseldi	|- ( ph -> C e. B )

Proof of Theorem sseldi

Step	Hyp	Ref	Expression
1		sseldi.2	. 2 |- ( ph -> C e. A )
2		sseli.1	. . 3 |- A C_ B
3	2	sseli 3057	. 2 |- ( C e. A -> C e. B )
4	1, 3	syl 14	1 |- ( ph -> C e. B )

Syntax hints:   -> wi 4   e. wcel 1461   C_ wss 3035

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-11 1465  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-in 3041  df-ss 3048

This theorem is referenced by:  mptrcl  5455  riotacl  5696  riotasbc  5697  elmpocl  5920  ofrval  5944  f1od2  6084  mpoxopn0yelv  6088  tpostpos  6113  smores  6141  supubti  6836  suplubti  6837  prarloclemcalc  7252  rereceu  7618  recriota  7619  rexrd  7733  eqord1  8158  nnred  8637  nncnd  8638  un0addcl  8908  un0mulcl  8909  nnnn0d  8928  nn0red  8929  nn0xnn0d  8947  suprzclex  9047  nn0zd  9069  zred  9071  rpred  9376  ige2m1fz  9777  zmodfzp1  10008  seq3caopr2  10142  expcl2lemap  10192  m1expcl  10203  summodclem2a  11036  zsumdc  11039  lcmn0cl  11589  ennnfonelemg  11755  lmrcl  12197  lmss  12251  upxp  12277  isxms2  12435  iooretopg  12511  tgqioo  12527  dvcl  12601  dvidlemap  12609  dvcnp2cntop  12612  isomninnlem  12906  trilpolemeq1  12914  trilpolemlt1  12915