Theorem sselid 3178

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

Syntax hints:   -> wi 4   e. wcel 2164   C_ wss 3154

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167

This theorem is referenced by:  mptrcl  5641  riotacl  5889  riotasbc  5890  elmpocl  6115  ofrval  6143  f1od2  6290  mpoxopn0yelv  6294  tpostpos  6319  smores  6347  supubti  7060  suplubti  7061  nninfwlporlemd  7233  nninfwlporlem  7234  nninfwlpoimlemg  7236  nninfwlpoimlemginf  7237  prarloclemcalc  7564  rereceu  7951  recriota  7952  rexrd  8071  eqord1  8504  nnred  8997  nncnd  8998  un0addcl  9276  un0mulcl  9277  nnnn0d  9296  nn0red  9297  nn0xnn0d  9315  suprzclex  9418  nn0zd  9440  zred  9442  rpred  9765  ige2m1fz  10179  zmodfzp1  10422  seq3caopr2  10567  seqf1oglem1  10593  seqf1oglem2  10594  expcl2lemap  10625  m1expcl  10636  summodclem2a  11527  zsumdc  11530  clim2prod  11685  ntrivcvgap  11694  prodmodclem2a  11722  zproddc  11725  zsupssdc  12094  nninfctlemfo  12180  lcmn0cl  12209  isprm5lem  12282  eulerthlemrprm  12370  eulerthlema  12371  eulerthlemh  12372  eulerthlemth  12373  prmdivdiv  12378  4sqlem13m  12544  4sqlem14  12545  4sqlem17  12548  ennnfonelemg  12563  relelbasov  12683  nmzsubg  13283  conjnmz  13352  conjnmzb  13353  rrgeq0  13764  znf1o  14150  lmrcl  14370  lmss  14425  upxp  14451  isxms2  14631  iooretopg  14707  tgqioo  14734  maxcncf  14794  mincncf  14795  ivthreinc  14824  limccoap  14857  dvcl  14862  dvidlemap  14870  dvidrelem  14871  dvidsslem  14872  dvconstss  14877  dvcnp2cntop  14878  plyaddcl  14933  plymulcl  14934  plysubcl  14935  wilthlem1  15153  lgscl  15171  lgsquadlem1  15234  lgsquadlem2  15235  2sqlem6  15277  2sqlem8  15280  2sqlem9  15281  isomninnlem  15590  trilpolemeq1  15600  trilpolemlt1  15601  iswomninnlem  15609  iswomni0  15611  ismkvnnlem  15612  nconstwlpolemgt0  15624