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  8811  nnred  9317  nncnd  9318  un0addcl  9596  un0mulcl  9597  nnnn0d  9620  nn0red  9621  nn0xnn0d  9639  suprzclex  9744  nn0zd  9766  zred  9768  rpred  10097  ige2m1fz  10517  zsupssdc  10673  zmodfzp1  10785  seq3caopr2  10930  seqf1oglem1  10956  seqf1oglem2  10957  expcl2lemap  10988  m1expcl  10999  ccatrn  11377  wrdind  11494  wrd2ind  11495  summodclem2a  12148  zsumdc  12151  clim2prod  12306  ntrivcvgap  12315  prodmodclem2a  12343  zproddc  12346  bitsfzolem  12721  nninfctlemfo  12817  lcmn0cl  12846  isprm5lem  12919  eulerthlemrprm  13007  eulerthlema  13008  eulerthlemh  13009  eulerthlemth  13010  prmdivdiv  13015  4sqlem13m  13182  4sqlem14  13183  4sqlem17  13186  ballotfilem2  13228  ballotfilemfrci  13271  ennnfonelemg  13294  relelbasov  13416  nmzsubg  14013  conjnmz  14082  conjnmzb  14083  rrgeq0  14573  znf1o  14986  psrbagconf1o  15064  mplelf  15088  mplsubgfilemcl  15090  mplsubgfileminv  15091  mpladd  15095  mplnegfi  15096  lmrcl  15293  lmss  15347  upxp  15373  isxms2  15553  iooretopg  15629  tgqioo  15656  maxcncf  15716  mincncf  15717  ivthreinc  15746  limccoap  15779  dvcl  15784  dvidlemap  15792  dvidrelem  15793  dvidsslem  15794  dvconstss  15799  dvcnp2cntop  15800  plyaddcl  15855  plymulcl  15856  plysubcl  15857  pellexlem3  16093  wilthlem1  16094  sgmval2  16098  mpodvdsmulf1o  16104  fsumdvdsmul  16105  sgmmul  16110  perfectlem2  16114  lgscl  16133  lgsquadlem1  16196  lgsquadlem2  16197  2sqlem6  16239  2sqlem8  16242  2sqlem9  16243  upgrss  16340  usgrss  16418  wlkres  16620  trlreslem  16630  isomninnlem  17079  trilpolemeq1  17089  trilpolemlt1  17090  iswomninnlem  17099  iswomni0  17101  ismkvnnlem  17102  nconstwlpolemgt0  17114