Theorem sselid 3246

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   C_ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  mptrcl  5791  fnfvimad  5957  riotacl  6057  riotasbc  6058  elmpocl  6287  ofrval  6317  f1od2  6475  elmpom  6478  mpoxopn0yelv  6514  tpostpos  6539  smores  6567  2omap  7324  supubti  7345  suplubti  7346  nninfwlporlemd  7518  nninfwlporlem  7519  nninfwlpoimlemg  7521  nninfwlpoimlemginf  7522  prarloclemcalc  7875  rereceu  8262  recriota  8263  rexrd  8381  eqord1  8818  nnred  9326  nncnd  9327  un0addcl  9607  un0mulcl  9608  nnnn0d  9631  nn0red  9632  nn0xnn0d  9650  suprzclex  9755  nn0zd  9777  zred  9779  rpred  10114  ige2m1fz  10534  zsupssdc  10690  zmodfzp1  10806  seq3caopr2  10951  seqf1oglem1  10977  seqf1oglem2  10978  expcl2lemap  11009  m1expcl  11020  ccatrn  11399  wrdind  11516  wrd2ind  11517  summodclem2a  12173  zsumdc  12176  clim2prod  12331  ntrivcvgap  12340  prodmodclem2a  12368  zproddc  12371  bitsfzolem  12746  nninfctlemfo  12842  lcmn0cl  12871  isprm5lem  12945  eulerthlemrprm  13036  eulerthlema  13037  eulerthlemh  13038  eulerthlemth  13039  prmdivdiv  13044  4sqlem13m  13211  4sqlem14  13212  4sqlem17  13215  ballotfilem2  13286  ballotfilemfrci  13329  ennnfonelemg  13352  relelbasov  13474  nmzsubg  14072  conjnmz  14141  conjnmzb  14142  cntzsgrpcl  14167  cntzsubm  14170  cntzsubg  14171  rrgeq0  14682  znf1o  15095  psrbagconf1o  15174  psrass1filem  15177  psrdifi  15202  psrdirfi  15203  mplelf  15213  mplsubgfilemcl  15215  mplsubgfileminv  15216  mpladd  15220  mplnegfi  15221  lmrcl  15418  lmss  15472  upxp  15498  isxms2  15678  iooretopg  15754  tgqioo  15781  maxcncf  15841  mincncf  15842  ivthreinc  15871  limccoap  15904  dvcl  15909  dvidlemap  15917  dvidrelem  15918  dvidsslem  15919  dvconstss  15924  dvcnp2cntop  15925  plyaddcl  15980  plymulcl  15981  plysubcl  15982  pellexlem3  16231  wilthlem1  16232  sgmval2  16253  mpodvdsmulf1o  16284  fsumdvdsmul  16285  sgmmul  16290  perfectlem2  16300  lgscl  16338  lgsquadlem1  16401  lgsquadlem2  16402  2sqlem6  16444  2sqlem8  16447  2sqlem9  16448  upgrss  16545  usgrss  16623  wlkres  16825  trlreslem  16835  idjudju  17252  isomninnlem  17285  trilpolemeq1  17296  trilpolemlt1  17297  iswomninnlem  17306  iswomni0  17308  ismkvnnlem  17309  nconstwlpolemgt0  17321