Theorem sselid 3195

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

Syntax hints:   → wi 4   ∈ wcel 2177   ⊆ wss 3170

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3176  df-ss 3183

This theorem is referenced by:  mptrcl  5675  riotacl  5927  riotasbc  5928  elmpocl  6154  ofrval  6182  f1od2  6334  mpoxopn0yelv  6338  tpostpos  6363  smores  6391  supubti  7116  suplubti  7117  nninfwlporlemd  7289  nninfwlporlem  7290  nninfwlpoimlemg  7292  nninfwlpoimlemginf  7293  prarloclemcalc  7635  rereceu  8022  recriota  8023  rexrd  8142  eqord1  8576  nnred  9069  nncnd  9070  un0addcl  9348  un0mulcl  9349  nnnn0d  9368  nn0red  9369  nn0xnn0d  9387  suprzclex  9491  nn0zd  9513  zred  9515  rpred  9838  ige2m1fz  10252  zsupssdc  10403  zmodfzp1  10515  seq3caopr2  10660  seqf1oglem1  10686  seqf1oglem2  10687  expcl2lemap  10718  m1expcl  10729  ccatrn  11088  wrdind  11198  wrd2ind  11199  summodclem2a  11767  zsumdc  11770  clim2prod  11925  ntrivcvgap  11934  prodmodclem2a  11962  zproddc  11965  bitsfzolem  12340  nninfctlemfo  12436  lcmn0cl  12465  isprm5lem  12538  eulerthlemrprm  12626  eulerthlema  12627  eulerthlemh  12628  eulerthlemth  12629  prmdivdiv  12634  4sqlem13m  12801  4sqlem14  12802  4sqlem17  12805  ennnfonelemg  12849  relelbasov  12969  nmzsubg  13621  conjnmz  13690  conjnmzb  13691  rrgeq0  14102  znf1o  14488  mplelf  14534  mplsubgfilemcl  14536  mplsubgfileminv  14537  mpladd  14541  mplnegfi  14542  lmrcl  14738  lmss  14793  upxp  14819  isxms2  14999  iooretopg  15075  tgqioo  15102  maxcncf  15162  mincncf  15163  ivthreinc  15192  limccoap  15225  dvcl  15230  dvidlemap  15238  dvidrelem  15239  dvidsslem  15240  dvconstss  15245  dvcnp2cntop  15246  plyaddcl  15301  plymulcl  15302  plysubcl  15303  wilthlem1  15527  sgmval2  15531  mpodvdsmulf1o  15537  fsumdvdsmul  15538  sgmmul  15543  perfectlem2  15547  lgscl  15566  lgsquadlem1  15629  lgsquadlem2  15630  2sqlem6  15672  2sqlem8  15675  2sqlem9  15676  upgrss  15770  2omap  16071  isomninnlem  16110  trilpolemeq1  16120  trilpolemlt1  16121  iswomninnlem  16129  iswomni0  16131  ismkvnnlem  16132  nconstwlpolemgt0  16144