Theorem sselid 3246

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

Syntax hints:   → wi 4   ∈ wcel 2209   ⊆ wss 3220

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  mptrcl  5782  fnfvimad  5944  riotacl  6044  riotasbc  6045  elmpocl  6274  ofrval  6303  f1od2  6461  elmpom  6464  mpoxopn0yelv  6500  tpostpos  6525  smores  6553  2omap  7308  supubti  7329  suplubti  7330  nninfwlporlemd  7502  nninfwlporlem  7503  nninfwlpoimlemg  7505  nninfwlpoimlemginf  7506  prarloclemcalc  7859  rereceu  8246  recriota  8247  rexrd  8365  eqord1  8801  nnred  9296  nncnd  9297  un0addcl  9575  un0mulcl  9576  nnnn0d  9599  nn0red  9600  nn0xnn0d  9618  suprzclex  9723  nn0zd  9745  zred  9747  rpred  10076  ige2m1fz  10495  zsupssdc  10651  zmodfzp1  10763  seq3caopr2  10908  seqf1oglem1  10934  seqf1oglem2  10935  expcl2lemap  10966  m1expcl  10977  ccatrn  11355  wrdind  11472  wrd2ind  11473  summodclem2a  12126  zsumdc  12129  clim2prod  12284  ntrivcvgap  12293  prodmodclem2a  12321  zproddc  12324  bitsfzolem  12699  nninfctlemfo  12795  lcmn0cl  12824  isprm5lem  12897  eulerthlemrprm  12985  eulerthlema  12986  eulerthlemh  12987  eulerthlemth  12988  prmdivdiv  12993  4sqlem13m  13160  4sqlem14  13161  4sqlem17  13164  ballotfilem2  13206  ballotfilemfrci  13249  ennnfonelemg  13272  relelbasov  13393  nmzsubg  13990  conjnmz  14059  conjnmzb  14060  rrgeq0  14546  znf1o  14958  psrbagconf1o  14987  mplelf  15011  mplsubgfilemcl  15013  mplsubgfileminv  15014  mpladd  15018  mplnegfi  15019  lmrcl  15216  lmss  15270  upxp  15296  isxms2  15476  iooretopg  15552  tgqioo  15579  maxcncf  15639  mincncf  15640  ivthreinc  15669  limccoap  15702  dvcl  15707  dvidlemap  15715  dvidrelem  15716  dvidsslem  15717  dvconstss  15722  dvcnp2cntop  15723  plyaddcl  15778  plymulcl  15779  plysubcl  15780  pellexlem3  16007  wilthlem1  16008  sgmval2  16012  mpodvdsmulf1o  16018  fsumdvdsmul  16019  sgmmul  16024  perfectlem2  16028  lgscl  16047  lgsquadlem1  16110  lgsquadlem2  16111  2sqlem6  16153  2sqlem8  16156  2sqlem9  16157  upgrss  16254  usgrss  16332  wlkres  16534  trlreslem  16544  isomninnlem  16984  trilpolemeq1  16994  trilpolemlt1  16995  iswomninnlem  17004  iswomni0  17006  ismkvnnlem  17007  nconstwlpolemgt0  17019