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  7319  supubti  7340  suplubti  7341  nninfwlporlemd  7513  nninfwlporlem  7514  nninfwlpoimlemg  7516  nninfwlpoimlemginf  7517  prarloclemcalc  7870  rereceu  8257  recriota  8258  rexrd  8376  eqord1  8813  nnred  9320  nncnd  9321  un0addcl  9601  un0mulcl  9602  nnnn0d  9625  nn0red  9626  nn0xnn0d  9644  suprzclex  9749  nn0zd  9771  zred  9773  rpred  10108  ige2m1fz  10528  zsupssdc  10684  zmodfzp1  10800  seq3caopr2  10945  seqf1oglem1  10971  seqf1oglem2  10972  expcl2lemap  11003  m1expcl  11014  ccatrn  11393  wrdind  11510  wrd2ind  11511  summodclem2a  12167  zsumdc  12170  clim2prod  12325  ntrivcvgap  12334  prodmodclem2a  12362  zproddc  12365  bitsfzolem  12740  nninfctlemfo  12836  lcmn0cl  12865  isprm5lem  12939  eulerthlemrprm  13030  eulerthlema  13031  eulerthlemh  13032  eulerthlemth  13033  prmdivdiv  13038  4sqlem13m  13205  4sqlem14  13206  4sqlem17  13209  ballotfilem2  13280  ballotfilemfrci  13323  ennnfonelemg  13346  relelbasov  13468  nmzsubg  14066  conjnmz  14135  conjnmzb  14136  cntzsgrpcl  14161  cntzsubm  14164  cntzsubg  14165  rrgeq0  14657  znf1o  15070  psrbagconf1o  15149  mplelf  15179  mplsubgfilemcl  15181  mplsubgfileminv  15182  mpladd  15186  mplnegfi  15187  lmrcl  15384  lmss  15438  upxp  15464  isxms2  15644  iooretopg  15720  tgqioo  15747  maxcncf  15807  mincncf  15808  ivthreinc  15837  limccoap  15870  dvcl  15875  dvidlemap  15883  dvidrelem  15884  dvidsslem  15885  dvconstss  15890  dvcnp2cntop  15891  plyaddcl  15946  plymulcl  15947  plysubcl  15948  pellexlem3  16192  wilthlem1  16193  sgmval2  16214  mpodvdsmulf1o  16245  fsumdvdsmul  16246  sgmmul  16251  perfectlem2  16261  lgscl  16299  lgsquadlem1  16362  lgsquadlem2  16363  2sqlem6  16405  2sqlem8  16408  2sqlem9  16409  upgrss  16506  usgrss  16584  wlkres  16786  trlreslem  16796  isomninnlem  17245  trilpolemeq1  17256  trilpolemlt1  17257  iswomninnlem  17266  iswomni0  17268  ismkvnnlem  17269  nconstwlpolemgt0  17281