Theorem sselid 3145

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

Syntax hints:   -> wi 4   e. wcel 2141   C_ wss 3121

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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  mptrcl  5578  riotacl  5823  riotasbc  5824  elmpocl  6047  ofrval  6071  f1od2  6214  mpoxopn0yelv  6218  tpostpos  6243  smores  6271  supubti  6976  suplubti  6977  nninfwlporlemd  7148  nninfwlporlem  7149  nninfwlpoimlemg  7151  nninfwlpoimlemginf  7152  prarloclemcalc  7464  rereceu  7851  recriota  7852  rexrd  7969  eqord1  8402  nnred  8891  nncnd  8892  un0addcl  9168  un0mulcl  9169  nnnn0d  9188  nn0red  9189  nn0xnn0d  9207  suprzclex  9310  nn0zd  9332  zred  9334  rpred  9653  ige2m1fz  10066  zmodfzp1  10304  seq3caopr2  10438  expcl2lemap  10488  m1expcl  10499  summodclem2a  11344  zsumdc  11347  clim2prod  11502  ntrivcvgap  11511  prodmodclem2a  11539  zproddc  11542  zsupssdc  11909  lcmn0cl  12022  isprm5lem  12095  eulerthlemrprm  12183  eulerthlema  12184  eulerthlemh  12185  eulerthlemth  12186  prmdivdiv  12191  ennnfonelemg  12358  lmrcl  12985  lmss  13040  upxp  13066  isxms2  13246  iooretopg  13322  tgqioo  13341  limccoap  13441  dvcl  13446  dvidlemap  13454  dvcnp2cntop  13457  lgscl  13709  2sqlem6  13750  2sqlem8  13753  2sqlem9  13754  isomninnlem  14062  trilpolemeq1  14072  trilpolemlt1  14073  iswomninnlem  14081  iswomni0  14083  ismkvnnlem  14084  nconstwlpolemgt0  14095