Theorem sselid 3223

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

Syntax hints:   → wi 4   ∈ wcel 2200   ⊆ wss 3198

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211

This theorem is referenced by:  mptrcl  5725  fnfvimad  5885  riotacl  5982  riotasbc  5983  elmpocl  6212  ofrval  6241  f1od2  6395  elmpom  6398  mpoxopn0yelv  6400  tpostpos  6425  smores  6453  supubti  7189  suplubti  7190  nninfwlporlemd  7362  nninfwlporlem  7363  nninfwlpoimlemg  7365  nninfwlpoimlemginf  7366  prarloclemcalc  7712  rereceu  8099  recriota  8100  rexrd  8219  eqord1  8653  nnred  9146  nncnd  9147  un0addcl  9425  un0mulcl  9426  nnnn0d  9445  nn0red  9446  nn0xnn0d  9464  suprzclex  9568  nn0zd  9590  zred  9592  rpred  9921  ige2m1fz  10335  zsupssdc  10488  zmodfzp1  10600  seq3caopr2  10745  seqf1oglem1  10771  seqf1oglem2  10772  expcl2lemap  10803  m1expcl  10814  ccatrn  11176  wrdind  11293  wrd2ind  11294  summodclem2a  11932  zsumdc  11935  clim2prod  12090  ntrivcvgap  12099  prodmodclem2a  12127  zproddc  12130  bitsfzolem  12505  nninfctlemfo  12601  lcmn0cl  12630  isprm5lem  12703  eulerthlemrprm  12791  eulerthlema  12792  eulerthlemh  12793  eulerthlemth  12794  prmdivdiv  12799  4sqlem13m  12966  4sqlem14  12967  4sqlem17  12970  ennnfonelemg  13014  relelbasov  13135  nmzsubg  13787  conjnmz  13856  conjnmzb  13857  rrgeq0  14269  znf1o  14655  mplelf  14701  mplsubgfilemcl  14703  mplsubgfileminv  14704  mpladd  14708  mplnegfi  14709  lmrcl  14906  lmss  14960  upxp  14986  isxms2  15166  iooretopg  15242  tgqioo  15269  maxcncf  15329  mincncf  15330  ivthreinc  15359  limccoap  15392  dvcl  15397  dvidlemap  15405  dvidrelem  15406  dvidsslem  15407  dvconstss  15412  dvcnp2cntop  15413  plyaddcl  15468  plymulcl  15469  plysubcl  15470  wilthlem1  15694  sgmval2  15698  mpodvdsmulf1o  15704  fsumdvdsmul  15705  sgmmul  15710  perfectlem2  15714  lgscl  15733  lgsquadlem1  15796  lgsquadlem2  15797  2sqlem6  15839  2sqlem8  15842  2sqlem9  15843  upgrss  15940  usgrss  16016  wlkres  16174  trlreslem  16184  2omap  16530  isomninnlem  16570  trilpolemeq1  16580  trilpolemlt1  16581  iswomninnlem  16589  iswomni0  16591  ismkvnnlem  16592  nconstwlpolemgt0  16604