Theorem sselid 3246

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209   ⊆ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  mptrcl  5788  fnfvimad  5954  riotacl  6054  riotasbc  6055  elmpocl  6284  ofrval  6313  f1od2  6471  elmpom  6474  mpoxopn0yelv  6510  tpostpos  6535  smores  6563  2omap  7318  supubti  7339  suplubti  7340  nninfwlporlemd  7512  nninfwlporlem  7513  nninfwlpoimlemg  7515  nninfwlpoimlemginf  7516  prarloclemcalc  7869  rereceu  8256  recriota  8257  rexrd  8375  eqord1  8812  nnred  9319  nncnd  9320  un0addcl  9600  un0mulcl  9601  nnnn0d  9624  nn0red  9625  nn0xnn0d  9643  suprzclex  9748  nn0zd  9770  zred  9772  rpred  10107  ige2m1fz  10527  zsupssdc  10683  zmodfzp1  10798  seq3caopr2  10943  seqf1oglem1  10969  seqf1oglem2  10970  expcl2lemap  11001  m1expcl  11012  ccatrn  11391  wrdind  11508  wrd2ind  11509  summodclem2a  12164  zsumdc  12167  clim2prod  12322  ntrivcvgap  12331  prodmodclem2a  12359  zproddc  12362  bitsfzolem  12737  nninfctlemfo  12833  lcmn0cl  12862  isprm5lem  12936  eulerthlemrprm  13027  eulerthlema  13028  eulerthlemh  13029  eulerthlemth  13030  prmdivdiv  13035  4sqlem13m  13202  4sqlem14  13203  4sqlem17  13206  ballotfilem2  13277  ballotfilemfrci  13320  ennnfonelemg  13343  relelbasov  13465  nmzsubg  14062  conjnmz  14131  conjnmzb  14132  rrgeq0  14622  znf1o  15035  psrbagconf1o  15113  mplelf  15137  mplsubgfilemcl  15139  mplsubgfileminv  15140  mpladd  15144  mplnegfi  15145  lmrcl  15342  lmss  15396  upxp  15422  isxms2  15602  iooretopg  15678  tgqioo  15705  maxcncf  15765  mincncf  15766  ivthreinc  15795  limccoap  15828  dvcl  15833  dvidlemap  15841  dvidrelem  15842  dvidsslem  15843  dvconstss  15848  dvcnp2cntop  15849  plyaddcl  15904  plymulcl  15905  plysubcl  15906  pellexlem3  16150  wilthlem1  16151  sgmval2  16165  mpodvdsmulf1o  16185  fsumdvdsmul  16186  sgmmul  16191  perfectlem2  16198  lgscl  16231  lgsquadlem1  16294  lgsquadlem2  16295  2sqlem6  16337  2sqlem8  16340  2sqlem9  16341  upgrss  16438  usgrss  16516  wlkres  16718  trlreslem  16728  isomninnlem  17177  trilpolemeq1  17187  trilpolemlt1  17188  iswomninnlem  17197  iswomni0  17199  ismkvnnlem  17200  nconstwlpolemgt0  17212