Theorem sselid 3240

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 3238	. 2 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)
4	1, 3	syl 14	1 ⊢ (𝜑 → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2205   ⊆ wss 3214

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 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  mptrcl  5765  fnfvimad  5927  riotacl  6027  riotasbc  6028  elmpocl  6257  ofrval  6286  f1od2  6444  elmpom  6447  mpoxopn0yelv  6483  tpostpos  6508  smores  6536  2omap  7282  supubti  7303  suplubti  7304  nninfwlporlemd  7476  nninfwlporlem  7477  nninfwlpoimlemg  7479  nninfwlpoimlemginf  7480  prarloclemcalc  7833  rereceu  8220  recriota  8221  rexrd  8339  eqord1  8774  nnred  9267  nncnd  9268  un0addcl  9546  un0mulcl  9547  nnnn0d  9570  nn0red  9571  nn0xnn0d  9589  suprzclex  9694  nn0zd  9716  zred  9718  rpred  10047  ige2m1fz  10466  zsupssdc  10622  zmodfzp1  10734  seq3caopr2  10879  seqf1oglem1  10905  seqf1oglem2  10906  expcl2lemap  10937  m1expcl  10948  ccatrn  11322  wrdind  11439  wrd2ind  11440  summodclem2a  12092  zsumdc  12095  clim2prod  12250  ntrivcvgap  12259  prodmodclem2a  12287  zproddc  12290  bitsfzolem  12665  nninfctlemfo  12761  lcmn0cl  12790  isprm5lem  12863  eulerthlemrprm  12951  eulerthlema  12952  eulerthlemh  12953  eulerthlemth  12954  prmdivdiv  12959  4sqlem13m  13126  4sqlem14  13127  4sqlem17  13130  ballotfilem2  13172  ballotfilemfrci  13215  ennnfonelemg  13238  relelbasov  13359  nmzsubg  13963  conjnmz  14032  conjnmzb  14033  rrgeq0  14511  znf1o  14925  psrbagconf1o  14954  mplelf  14978  mplsubgfilemcl  14980  mplsubgfileminv  14981  mpladd  14985  mplnegfi  14986  lmrcl  15183  lmss  15237  upxp  15263  isxms2  15443  iooretopg  15519  tgqioo  15546  maxcncf  15606  mincncf  15607  ivthreinc  15636  limccoap  15669  dvcl  15674  dvidlemap  15682  dvidrelem  15683  dvidsslem  15684  dvconstss  15689  dvcnp2cntop  15690  plyaddcl  15745  plymulcl  15746  plysubcl  15747  pellexlem3  15973  wilthlem1  15974  sgmval2  15978  mpodvdsmulf1o  15984  fsumdvdsmul  15985  sgmmul  15990  perfectlem2  15994  lgscl  16013  lgsquadlem1  16076  lgsquadlem2  16077  2sqlem6  16119  2sqlem8  16122  2sqlem9  16123  upgrss  16220  usgrss  16298  wlkres  16500  trlreslem  16510  isomninnlem  16940  trilpolemeq1  16950  trilpolemlt1  16951  iswomninnlem  16960  iswomni0  16962  ismkvnnlem  16963  nconstwlpolemgt0  16976