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  5716  riotacl  5969  riotasbc  5970  elmpocl  6199  ofrval  6227  f1od2  6379  mpoxopn0yelv  6383  tpostpos  6408  smores  6436  supubti  7162  suplubti  7163  nninfwlporlemd  7335  nninfwlporlem  7336  nninfwlpoimlemg  7338  nninfwlpoimlemginf  7339  prarloclemcalc  7685  rereceu  8072  recriota  8073  rexrd  8192  eqord1  8626  nnred  9119  nncnd  9120  un0addcl  9398  un0mulcl  9399  nnnn0d  9418  nn0red  9419  nn0xnn0d  9437  suprzclex  9541  nn0zd  9563  zred  9565  rpred  9888  ige2m1fz  10302  zsupssdc  10453  zmodfzp1  10565  seq3caopr2  10710  seqf1oglem1  10736  seqf1oglem2  10737  expcl2lemap  10768  m1expcl  10779  ccatrn  11139  wrdind  11249  wrd2ind  11250  summodclem2a  11887  zsumdc  11890  clim2prod  12045  ntrivcvgap  12054  prodmodclem2a  12082  zproddc  12085  bitsfzolem  12460  nninfctlemfo  12556  lcmn0cl  12585  isprm5lem  12658  eulerthlemrprm  12746  eulerthlema  12747  eulerthlemh  12748  eulerthlemth  12749  prmdivdiv  12754  4sqlem13m  12921  4sqlem14  12922  4sqlem17  12925  ennnfonelemg  12969  relelbasov  13090  nmzsubg  13742  conjnmz  13811  conjnmzb  13812  rrgeq0  14223  znf1o  14609  mplelf  14655  mplsubgfilemcl  14657  mplsubgfileminv  14658  mpladd  14662  mplnegfi  14663  lmrcl  14859  lmss  14914  upxp  14940  isxms2  15120  iooretopg  15196  tgqioo  15223  maxcncf  15283  mincncf  15284  ivthreinc  15313  limccoap  15346  dvcl  15351  dvidlemap  15359  dvidrelem  15360  dvidsslem  15361  dvconstss  15366  dvcnp2cntop  15367  plyaddcl  15422  plymulcl  15423  plysubcl  15424  wilthlem1  15648  sgmval2  15652  mpodvdsmulf1o  15658  fsumdvdsmul  15659  sgmmul  15664  perfectlem2  15668  lgscl  15687  lgsquadlem1  15750  lgsquadlem2  15751  2sqlem6  15793  2sqlem8  15796  2sqlem9  15797  upgrss  15893  usgrss  15969  2omap  16318  isomninnlem  16357  trilpolemeq1  16367  trilpolemlt1  16368  iswomninnlem  16376  iswomni0  16378  ismkvnnlem  16379  nconstwlpolemgt0  16391