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  7258  suplubti  7259  nninfwlporlemd  7431  nninfwlporlem  7432  nninfwlpoimlemg  7434  nninfwlpoimlemginf  7435  prarloclemcalc  7782  rereceu  8169  recriota  8170  rexrd  8288  eqord1  8722  nnred  9215  nncnd  9216  un0addcl  9494  un0mulcl  9495  nnnn0d  9516  nn0red  9517  nn0xnn0d  9535  suprzclex  9639  nn0zd  9661  zred  9663  rpred  9992  ige2m1fz  10407  zsupssdc  10561  zmodfzp1  10673  seq3caopr2  10818  seqf1oglem1  10844  seqf1oglem2  10845  expcl2lemap  10876  m1expcl  10887  ccatrn  11252  wrdind  11369  wrd2ind  11370  summodclem2a  12022  zsumdc  12025  clim2prod  12180  ntrivcvgap  12189  prodmodclem2a  12217  zproddc  12220  bitsfzolem  12595  nninfctlemfo  12691  lcmn0cl  12720  isprm5lem  12793  eulerthlemrprm  12881  eulerthlema  12882  eulerthlemh  12883  eulerthlemth  12884  prmdivdiv  12889  4sqlem13m  13056  4sqlem14  13057  4sqlem17  13060  ennnfonelemg  13104  relelbasov  13225  nmzsubg  13877  conjnmz  13946  conjnmzb  13947  rrgeq0  14360  znf1o  14747  psrbagconf1o  14774  mplelf  14798  mplsubgfilemcl  14800  mplsubgfileminv  14801  mpladd  14805  mplnegfi  14806  lmrcl  15003  lmss  15057  upxp  15083  isxms2  15263  iooretopg  15339  tgqioo  15366  maxcncf  15426  mincncf  15427  ivthreinc  15456  limccoap  15489  dvcl  15494  dvidlemap  15502  dvidrelem  15503  dvidsslem  15504  dvconstss  15509  dvcnp2cntop  15510  plyaddcl  15565  plymulcl  15566  plysubcl  15567  pellexlem3  15793  wilthlem1  15794  sgmval2  15798  mpodvdsmulf1o  15804  fsumdvdsmul  15805  sgmmul  15810  perfectlem2  15814  lgscl  15833  lgsquadlem1  15896  lgsquadlem2  15897  2sqlem6  15939  2sqlem8  15942  2sqlem9  15943  upgrss  16040  usgrss  16118  wlkres  16320  trlreslem  16330  2omap  16715  isomninnlem  16762  trilpolemeq1  16772  trilpolemlt1  16773  iswomninnlem  16782  iswomni0  16784  ismkvnnlem  16785  nconstwlpolemgt0  16797