Theorem sselid 3182

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

Syntax hints:   → wi 4   ∈ wcel 2167   ⊆ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  mptrcl  5647  riotacl  5895  riotasbc  5896  elmpocl  6122  ofrval  6150  f1od2  6302  mpoxopn0yelv  6306  tpostpos  6331  smores  6359  supubti  7074  suplubti  7075  nninfwlporlemd  7247  nninfwlporlem  7248  nninfwlpoimlemg  7250  nninfwlpoimlemginf  7251  prarloclemcalc  7588  rereceu  7975  recriota  7976  rexrd  8095  eqord1  8529  nnred  9022  nncnd  9023  un0addcl  9301  un0mulcl  9302  nnnn0d  9321  nn0red  9322  nn0xnn0d  9340  suprzclex  9443  nn0zd  9465  zred  9467  rpred  9790  ige2m1fz  10204  zsupssdc  10347  zmodfzp1  10459  seq3caopr2  10604  seqf1oglem1  10630  seqf1oglem2  10631  expcl2lemap  10662  m1expcl  10673  summodclem2a  11565  zsumdc  11568  clim2prod  11723  ntrivcvgap  11732  prodmodclem2a  11760  zproddc  11763  bitsfzolem  12138  nninfctlemfo  12234  lcmn0cl  12263  isprm5lem  12336  eulerthlemrprm  12424  eulerthlema  12425  eulerthlemh  12426  eulerthlemth  12427  prmdivdiv  12432  4sqlem13m  12599  4sqlem14  12600  4sqlem17  12603  ennnfonelemg  12647  relelbasov  12767  nmzsubg  13418  conjnmz  13487  conjnmzb  13488  rrgeq0  13899  znf1o  14285  mplelf  14331  mplsubgfilemcl  14333  mplsubgfileminv  14334  mpladd  14338  mplnegfi  14339  lmrcl  14535  lmss  14590  upxp  14616  isxms2  14796  iooretopg  14872  tgqioo  14899  maxcncf  14959  mincncf  14960  ivthreinc  14989  limccoap  15022  dvcl  15027  dvidlemap  15035  dvidrelem  15036  dvidsslem  15037  dvconstss  15042  dvcnp2cntop  15043  plyaddcl  15098  plymulcl  15099  plysubcl  15100  wilthlem1  15324  sgmval2  15328  mpodvdsmulf1o  15334  fsumdvdsmul  15335  sgmmul  15340  perfectlem2  15344  lgscl  15363  lgsquadlem1  15426  lgsquadlem2  15427  2sqlem6  15469  2sqlem8  15472  2sqlem9  15473  2omap  15750  isomninnlem  15787  trilpolemeq1  15797  trilpolemlt1  15798  iswomninnlem  15806  iswomni0  15808  ismkvnnlem  15809  nconstwlpolemgt0  15821