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  5661  riotacl  5913  riotasbc  5914  elmpocl  6140  ofrval  6168  f1od2  6320  mpoxopn0yelv  6324  tpostpos  6349  smores  6377  supubti  7100  suplubti  7101  nninfwlporlemd  7273  nninfwlporlem  7274  nninfwlpoimlemg  7276  nninfwlpoimlemginf  7277  prarloclemcalc  7614  rereceu  8001  recriota  8002  rexrd  8121  eqord1  8555  nnred  9048  nncnd  9049  un0addcl  9327  un0mulcl  9328  nnnn0d  9347  nn0red  9348  nn0xnn0d  9366  suprzclex  9470  nn0zd  9492  zred  9494  rpred  9817  ige2m1fz  10231  zsupssdc  10379  zmodfzp1  10491  seq3caopr2  10636  seqf1oglem1  10662  seqf1oglem2  10663  expcl2lemap  10694  m1expcl  10705  ccatrn  11063  summodclem2a  11634  zsumdc  11637  clim2prod  11792  ntrivcvgap  11801  prodmodclem2a  11829  zproddc  11832  bitsfzolem  12207  nninfctlemfo  12303  lcmn0cl  12332  isprm5lem  12405  eulerthlemrprm  12493  eulerthlema  12494  eulerthlemh  12495  eulerthlemth  12496  prmdivdiv  12501  4sqlem13m  12668  4sqlem14  12669  4sqlem17  12672  ennnfonelemg  12716  relelbasov  12836  nmzsubg  13488  conjnmz  13557  conjnmzb  13558  rrgeq0  13969  znf1o  14355  mplelf  14401  mplsubgfilemcl  14403  mplsubgfileminv  14404  mpladd  14408  mplnegfi  14409  lmrcl  14605  lmss  14660  upxp  14686  isxms2  14866  iooretopg  14942  tgqioo  14969  maxcncf  15029  mincncf  15030  ivthreinc  15059  limccoap  15092  dvcl  15097  dvidlemap  15105  dvidrelem  15106  dvidsslem  15107  dvconstss  15112  dvcnp2cntop  15113  plyaddcl  15168  plymulcl  15169  plysubcl  15170  wilthlem1  15394  sgmval2  15398  mpodvdsmulf1o  15404  fsumdvdsmul  15405  sgmmul  15410  perfectlem2  15414  lgscl  15433  lgsquadlem1  15496  lgsquadlem2  15497  2sqlem6  15539  2sqlem8  15542  2sqlem9  15543  2omap  15865  isomninnlem  15902  trilpolemeq1  15912  trilpolemlt1  15913  iswomninnlem  15921  iswomni0  15923  ismkvnnlem  15924  nconstwlpolemgt0  15936