Theorem sselid 3190

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

Syntax hints:   → wi 4   ∈ wcel 2175   ⊆ wss 3165

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-in 3171  df-ss 3178

This theorem is referenced by:  mptrcl  5656  riotacl  5904  riotasbc  5905  elmpocl  6131  ofrval  6159  f1od2  6311  mpoxopn0yelv  6315  tpostpos  6340  smores  6368  supubti  7083  suplubti  7084  nninfwlporlemd  7256  nninfwlporlem  7257  nninfwlpoimlemg  7259  nninfwlpoimlemginf  7260  prarloclemcalc  7597  rereceu  7984  recriota  7985  rexrd  8104  eqord1  8538  nnred  9031  nncnd  9032  un0addcl  9310  un0mulcl  9311  nnnn0d  9330  nn0red  9331  nn0xnn0d  9349  suprzclex  9453  nn0zd  9475  zred  9477  rpred  9800  ige2m1fz  10214  zsupssdc  10362  zmodfzp1  10474  seq3caopr2  10619  seqf1oglem1  10645  seqf1oglem2  10646  expcl2lemap  10677  m1expcl  10688  ccatrn  11040  summodclem2a  11611  zsumdc  11614  clim2prod  11769  ntrivcvgap  11778  prodmodclem2a  11806  zproddc  11809  bitsfzolem  12184  nninfctlemfo  12280  lcmn0cl  12309  isprm5lem  12382  eulerthlemrprm  12470  eulerthlema  12471  eulerthlemh  12472  eulerthlemth  12473  prmdivdiv  12478  4sqlem13m  12645  4sqlem14  12646  4sqlem17  12649  ennnfonelemg  12693  relelbasov  12813  nmzsubg  13464  conjnmz  13533  conjnmzb  13534  rrgeq0  13945  znf1o  14331  mplelf  14377  mplsubgfilemcl  14379  mplsubgfileminv  14380  mpladd  14384  mplnegfi  14385  lmrcl  14581  lmss  14636  upxp  14662  isxms2  14842  iooretopg  14918  tgqioo  14945  maxcncf  15005  mincncf  15006  ivthreinc  15035  limccoap  15068  dvcl  15073  dvidlemap  15081  dvidrelem  15082  dvidsslem  15083  dvconstss  15088  dvcnp2cntop  15089  plyaddcl  15144  plymulcl  15145  plysubcl  15146  wilthlem1  15370  sgmval2  15374  mpodvdsmulf1o  15380  fsumdvdsmul  15381  sgmmul  15386  perfectlem2  15390  lgscl  15409  lgsquadlem1  15472  lgsquadlem2  15473  2sqlem6  15515  2sqlem8  15518  2sqlem9  15519  2omap  15796  isomninnlem  15833  trilpolemeq1  15843  trilpolemlt1  15844  iswomninnlem  15852  iswomni0  15854  ismkvnnlem  15855  nconstwlpolemgt0  15867