Theorem sselid 3222

Description: Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.)

Hypotheses

Ref	Expression
sseli.1	⊢ 𝐴 ⊆ 𝐵
sselid.2	⊢ (𝜑 → 𝐶 ∈ 𝐴)

Assertion

Ref	Expression
sselid	⊢ (𝜑 → 𝐶 ∈ 𝐵)

Proof of Theorem sselid

Step	Hyp	Ref	Expression
1		sselid.2	. 2 ⊢ (𝜑 → 𝐶 ∈ 𝐴)
2		sseli.1	. . 3 ⊢ 𝐴 ⊆ 𝐵
3	2	sseli 3220	. 2 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)
4	1, 3	syl 14	1 ⊢ (𝜑 → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2200   ⊆ 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  11269  wrd2ind  11270  summodclem2a  11907  zsumdc  11910  clim2prod  12065  ntrivcvgap  12074  prodmodclem2a  12102  zproddc  12105  bitsfzolem  12480  nninfctlemfo  12576  lcmn0cl  12605  isprm5lem  12678  eulerthlemrprm  12766  eulerthlema  12767  eulerthlemh  12768  eulerthlemth  12769  prmdivdiv  12774  4sqlem13m  12941  4sqlem14  12942  4sqlem17  12945  ennnfonelemg  12989  relelbasov  13110  nmzsubg  13762  conjnmz  13831  conjnmzb  13832  rrgeq0  14244  znf1o  14630  mplelf  14676  mplsubgfilemcl  14678  mplsubgfileminv  14679  mpladd  14683  mplnegfi  14684  lmrcl  14881  lmss  14935  upxp  14961  isxms2  15141  iooretopg  15217  tgqioo  15244  maxcncf  15304  mincncf  15305  ivthreinc  15334  limccoap  15367  dvcl  15372  dvidlemap  15380  dvidrelem  15381  dvidsslem  15382  dvconstss  15387  dvcnp2cntop  15388  plyaddcl  15443  plymulcl  15444  plysubcl  15445  wilthlem1  15669  sgmval2  15673  mpodvdsmulf1o  15679  fsumdvdsmul  15680  sgmmul  15685  perfectlem2  15689  lgscl  15708  lgsquadlem1  15771  lgsquadlem2  15772  2sqlem6  15814  2sqlem8  15817  2sqlem9  15818  upgrss  15914  usgrss  15990  wlkres  16118  trlreslem  16127  2omap  16418  isomninnlem  16458  trilpolemeq1  16468  trilpolemlt1  16469  iswomninnlem  16477  iswomni0  16479  ismkvnnlem  16480  nconstwlpolemgt0  16492