Theorem sselid 3226

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

Syntax hints:   → wi 4   ∈ wcel 2202   ⊆ wss 3201

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  mptrcl  5738  fnfvimad  5900  riotacl  5997  riotasbc  5998  elmpocl  6227  ofrval  6255  f1od2  6409  elmpom  6412  mpoxopn0yelv  6448  tpostpos  6473  smores  6501  supubti  7241  suplubti  7242  nninfwlporlemd  7414  nninfwlporlem  7415  nninfwlpoimlemg  7417  nninfwlpoimlemginf  7418  prarloclemcalc  7765  rereceu  8152  recriota  8153  rexrd  8271  eqord1  8705  nnred  9198  nncnd  9199  un0addcl  9477  un0mulcl  9478  nnnn0d  9499  nn0red  9500  nn0xnn0d  9518  suprzclex  9622  nn0zd  9644  zred  9646  rpred  9975  ige2m1fz  10390  zsupssdc  10544  zmodfzp1  10656  seq3caopr2  10801  seqf1oglem1  10827  seqf1oglem2  10828  expcl2lemap  10859  m1expcl  10870  ccatrn  11235  wrdind  11352  wrd2ind  11353  summodclem2a  12005  zsumdc  12008  clim2prod  12163  ntrivcvgap  12172  prodmodclem2a  12200  zproddc  12203  bitsfzolem  12578  nninfctlemfo  12674  lcmn0cl  12703  isprm5lem  12776  eulerthlemrprm  12864  eulerthlema  12865  eulerthlemh  12866  eulerthlemth  12867  prmdivdiv  12872  4sqlem13m  13039  4sqlem14  13040  4sqlem17  13043  ennnfonelemg  13087  relelbasov  13208  nmzsubg  13860  conjnmz  13929  conjnmzb  13930  rrgeq0  14343  znf1o  14730  psrbagconf1o  14757  mplelf  14781  mplsubgfilemcl  14783  mplsubgfileminv  14784  mpladd  14788  mplnegfi  14789  lmrcl  14986  lmss  15040  upxp  15066  isxms2  15246  iooretopg  15322  tgqioo  15349  maxcncf  15409  mincncf  15410  ivthreinc  15439  limccoap  15472  dvcl  15477  dvidlemap  15485  dvidrelem  15486  dvidsslem  15487  dvconstss  15492  dvcnp2cntop  15493  plyaddcl  15548  plymulcl  15549  plysubcl  15550  pellexlem3  15776  wilthlem1  15777  sgmval2  15781  mpodvdsmulf1o  15787  fsumdvdsmul  15788  sgmmul  15793  perfectlem2  15797  lgscl  15816  lgsquadlem1  15879  lgsquadlem2  15880  2sqlem6  15922  2sqlem8  15925  2sqlem9  15926  upgrss  16023  usgrss  16101  wlkres  16303  trlreslem  16313  2omap  16698  isomninnlem  16745  trilpolemeq1  16755  trilpolemlt1  16756  iswomninnlem  16765  iswomni0  16767  ismkvnnlem  16768  nconstwlpolemgt0  16780