Theorem sseldi 3135

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

Syntax hints:   -> wi 4   e. wcel 2135   C_ wss 3111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-11 1493  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-in 3117  df-ss 3124

This theorem is referenced by:  mptrcl  5562  riotacl  5806  riotasbc  5807  elmpocl  6030  ofrval  6054  f1od2  6194  mpoxopn0yelv  6198  tpostpos  6223  smores  6251  supubti  6955  suplubti  6956  prarloclemcalc  7434  rereceu  7821  recriota  7822  rexrd  7939  eqord1  8372  nnred  8861  nncnd  8862  un0addcl  9138  un0mulcl  9139  nnnn0d  9158  nn0red  9159  nn0xnn0d  9177  suprzclex  9280  nn0zd  9302  zred  9304  rpred  9623  ige2m1fz  10035  zmodfzp1  10273  seq3caopr2  10407  expcl2lemap  10457  m1expcl  10468  summodclem2a  11308  zsumdc  11311  clim2prod  11466  ntrivcvgap  11475  prodmodclem2a  11503  zproddc  11506  zsupssdc  11872  lcmn0cl  11979  eulerthlemrprm  12138  eulerthlema  12139  eulerthlemh  12140  eulerthlemth  12141  prmdivdiv  12146  ennnfonelemg  12273  lmrcl  12732  lmss  12787  upxp  12813  isxms2  12993  iooretopg  13069  tgqioo  13088  limccoap  13188  dvcl  13193  dvidlemap  13201  dvcnp2cntop  13204  isomninnlem  13743  trilpolemeq1  13753  trilpolemlt1  13754  iswomninnlem  13762  iswomni0  13764  ismkvnnlem  13765  nconstwlpolemgt0  13776