Theorem sselid 3222

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

Syntax hints:   -> wi 4   e. wcel 2200   C_ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  mptrcl  5719  fnfvimad  5879  riotacl  5976  riotasbc  5977  elmpocl  6206  ofrval  6235  f1od2  6387  mpoxopn0yelv  6391  tpostpos  6416  smores  6444  supubti  7177  suplubti  7178  nninfwlporlemd  7350  nninfwlporlem  7351  nninfwlpoimlemg  7353  nninfwlpoimlemginf  7354  prarloclemcalc  7700  rereceu  8087  recriota  8088  rexrd  8207  eqord1  8641  nnred  9134  nncnd  9135  un0addcl  9413  un0mulcl  9414  nnnn0d  9433  nn0red  9434  nn0xnn0d  9452  suprzclex  9556  nn0zd  9578  zred  9580  rpred  9904  ige2m1fz  10318  zsupssdc  10470  zmodfzp1  10582  seq3caopr2  10727  seqf1oglem1  10753  seqf1oglem2  10754  expcl2lemap  10785  m1expcl  10796  ccatrn  11157  wrdind  11270  wrd2ind  11271  summodclem2a  11908  zsumdc  11911  clim2prod  12066  ntrivcvgap  12075  prodmodclem2a  12103  zproddc  12106  bitsfzolem  12481  nninfctlemfo  12577  lcmn0cl  12606  isprm5lem  12679  eulerthlemrprm  12767  eulerthlema  12768  eulerthlemh  12769  eulerthlemth  12770  prmdivdiv  12775  4sqlem13m  12942  4sqlem14  12943  4sqlem17  12946  ennnfonelemg  12990  relelbasov  13111  nmzsubg  13763  conjnmz  13832  conjnmzb  13833  rrgeq0  14245  znf1o  14631  mplelf  14677  mplsubgfilemcl  14679  mplsubgfileminv  14680  mpladd  14684  mplnegfi  14685  lmrcl  14882  lmss  14936  upxp  14962  isxms2  15142  iooretopg  15218  tgqioo  15245  maxcncf  15305  mincncf  15306  ivthreinc  15335  limccoap  15368  dvcl  15373  dvidlemap  15381  dvidrelem  15382  dvidsslem  15383  dvconstss  15388  dvcnp2cntop  15389  plyaddcl  15444  plymulcl  15445  plysubcl  15446  wilthlem1  15670  sgmval2  15674  mpodvdsmulf1o  15680  fsumdvdsmul  15681  sgmmul  15686  perfectlem2  15690  lgscl  15709  lgsquadlem1  15772  lgsquadlem2  15773  2sqlem6  15815  2sqlem8  15818  2sqlem9  15819  upgrss  15915  usgrss  15991  wlkres  16123  trlreslem  16132  2omap  16446  isomninnlem  16486  trilpolemeq1  16496  trilpolemlt1  16497  iswomninnlem  16505  iswomni0  16507  ismkvnnlem  16508  nconstwlpolemgt0  16520