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  5890  riotacl  5987  riotasbc  5988  elmpocl  6217  ofrval  6246  f1od2  6400  elmpom  6403  mpoxopn0yelv  6405  tpostpos  6430  smores  6458  supubti  7198  suplubti  7199  nninfwlporlemd  7371  nninfwlporlem  7372  nninfwlpoimlemg  7374  nninfwlpoimlemginf  7375  prarloclemcalc  7722  rereceu  8109  recriota  8110  rexrd  8229  eqord1  8663  nnred  9156  nncnd  9157  un0addcl  9435  un0mulcl  9436  nnnn0d  9455  nn0red  9456  nn0xnn0d  9474  suprzclex  9578  nn0zd  9600  zred  9602  rpred  9931  ige2m1fz  10345  zsupssdc  10499  zmodfzp1  10611  seq3caopr2  10756  seqf1oglem1  10782  seqf1oglem2  10783  expcl2lemap  10814  m1expcl  10825  ccatrn  11190  wrdind  11307  wrd2ind  11308  summodclem2a  11947  zsumdc  11950  clim2prod  12105  ntrivcvgap  12114  prodmodclem2a  12142  zproddc  12145  bitsfzolem  12520  nninfctlemfo  12616  lcmn0cl  12645  isprm5lem  12718  eulerthlemrprm  12806  eulerthlema  12807  eulerthlemh  12808  eulerthlemth  12809  prmdivdiv  12814  4sqlem13m  12981  4sqlem14  12982  4sqlem17  12985  ennnfonelemg  13029  relelbasov  13150  nmzsubg  13802  conjnmz  13871  conjnmzb  13872  rrgeq0  14285  znf1o  14671  mplelf  14717  mplsubgfilemcl  14719  mplsubgfileminv  14720  mpladd  14724  mplnegfi  14725  lmrcl  14922  lmss  14976  upxp  15002  isxms2  15182  iooretopg  15258  tgqioo  15285  maxcncf  15345  mincncf  15346  ivthreinc  15375  limccoap  15408  dvcl  15413  dvidlemap  15421  dvidrelem  15422  dvidsslem  15423  dvconstss  15428  dvcnp2cntop  15429  plyaddcl  15484  plymulcl  15485  plysubcl  15486  wilthlem1  15710  sgmval2  15714  mpodvdsmulf1o  15720  fsumdvdsmul  15721  sgmmul  15726  perfectlem2  15730  lgscl  15749  lgsquadlem1  15812  lgsquadlem2  15813  2sqlem6  15855  2sqlem8  15858  2sqlem9  15859  upgrss  15956  usgrss  16034  wlkres  16236  trlreslem  16246  2omap  16620  isomninnlem  16660  trilpolemeq1  16670  trilpolemlt1  16671  iswomninnlem  16680  iswomni0  16682  ismkvnnlem  16683  nconstwlpolemgt0  16695