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  7586  rereceu  7973  recriota  7974  rexrd  8093  eqord1  8527  nnred  9020  nncnd  9021  un0addcl  9299  un0mulcl  9300  nnnn0d  9319  nn0red  9320  nn0xnn0d  9338  suprzclex  9441  nn0zd  9463  zred  9465  rpred  9788  ige2m1fz  10202  zsupssdc  10345  zmodfzp1  10457  seq3caopr2  10602  seqf1oglem1  10628  seqf1oglem2  10629  expcl2lemap  10660  m1expcl  10671  summodclem2a  11563  zsumdc  11566  clim2prod  11721  ntrivcvgap  11730  prodmodclem2a  11758  zproddc  11761  bitsfzolem  12136  nninfctlemfo  12232  lcmn0cl  12261  isprm5lem  12334  eulerthlemrprm  12422  eulerthlema  12423  eulerthlemh  12424  eulerthlemth  12425  prmdivdiv  12430  4sqlem13m  12597  4sqlem14  12598  4sqlem17  12601  ennnfonelemg  12645  relelbasov  12765  nmzsubg  13416  conjnmz  13485  conjnmzb  13486  rrgeq0  13897  znf1o  14283  lmrcl  14511  lmss  14566  upxp  14592  isxms2  14772  iooretopg  14848  tgqioo  14875  maxcncf  14935  mincncf  14936  ivthreinc  14965  limccoap  14998  dvcl  15003  dvidlemap  15011  dvidrelem  15012  dvidsslem  15013  dvconstss  15018  dvcnp2cntop  15019  plyaddcl  15074  plymulcl  15075  plysubcl  15076  wilthlem1  15300  sgmval2  15304  mpodvdsmulf1o  15310  fsumdvdsmul  15311  sgmmul  15316  perfectlem2  15320  lgscl  15339  lgsquadlem1  15402  lgsquadlem2  15403  2sqlem6  15445  2sqlem8  15448  2sqlem9  15449  2omap  15726  isomninnlem  15761  trilpolemeq1  15771  trilpolemlt1  15772  iswomninnlem  15780  iswomni0  15782  ismkvnnlem  15783  nconstwlpolemgt0  15795