Theorem sselid 3225

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

Syntax hints:   → wi 4   ∈ wcel 2202   ⊆ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  mptrcl  5729  fnfvimad  5889  riotacl  5986  riotasbc  5987  elmpocl  6216  ofrval  6245  f1od2  6399  elmpom  6402  mpoxopn0yelv  6404  tpostpos  6429  smores  6457  supubti  7197  suplubti  7198  nninfwlporlemd  7370  nninfwlporlem  7371  nninfwlpoimlemg  7373  nninfwlpoimlemginf  7374  prarloclemcalc  7721  rereceu  8108  recriota  8109  rexrd  8228  eqord1  8662  nnred  9155  nncnd  9156  un0addcl  9434  un0mulcl  9435  nnnn0d  9454  nn0red  9455  nn0xnn0d  9473  suprzclex  9577  nn0zd  9599  zred  9601  rpred  9930  ige2m1fz  10344  zsupssdc  10497  zmodfzp1  10609  seq3caopr2  10754  seqf1oglem1  10780  seqf1oglem2  10781  expcl2lemap  10812  m1expcl  10823  ccatrn  11185  wrdind  11302  wrd2ind  11303  summodclem2a  11941  zsumdc  11944  clim2prod  12099  ntrivcvgap  12108  prodmodclem2a  12136  zproddc  12139  bitsfzolem  12514  nninfctlemfo  12610  lcmn0cl  12639  isprm5lem  12712  eulerthlemrprm  12800  eulerthlema  12801  eulerthlemh  12802  eulerthlemth  12803  prmdivdiv  12808  4sqlem13m  12975  4sqlem14  12976  4sqlem17  12979  ennnfonelemg  13023  relelbasov  13144  nmzsubg  13796  conjnmz  13865  conjnmzb  13866  rrgeq0  14278  znf1o  14664  mplelf  14710  mplsubgfilemcl  14712  mplsubgfileminv  14713  mpladd  14717  mplnegfi  14718  lmrcl  14915  lmss  14969  upxp  14995  isxms2  15175  iooretopg  15251  tgqioo  15278  maxcncf  15338  mincncf  15339  ivthreinc  15368  limccoap  15401  dvcl  15406  dvidlemap  15414  dvidrelem  15415  dvidsslem  15416  dvconstss  15421  dvcnp2cntop  15422  plyaddcl  15477  plymulcl  15478  plysubcl  15479  wilthlem1  15703  sgmval2  15707  mpodvdsmulf1o  15713  fsumdvdsmul  15714  sgmmul  15719  perfectlem2  15723  lgscl  15742  lgsquadlem1  15805  lgsquadlem2  15806  2sqlem6  15848  2sqlem8  15851  2sqlem9  15852  upgrss  15949  usgrss  16027  wlkres  16229  trlreslem  16239  2omap  16594  isomninnlem  16634  trilpolemeq1  16644  trilpolemlt1  16645  iswomninnlem  16653  iswomni0  16655  ismkvnnlem  16656  nconstwlpolemgt0  16668