Theorem sseldi 3045

Description: Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.)

Hypotheses

Ref	Expression
sseli.1	⊢ 𝐴 ⊆ 𝐵
sseldi.2	⊢ (𝜑 → 𝐶 ∈ 𝐴)

Assertion

Ref	Expression
sseldi	⊢ (𝜑 → 𝐶 ∈ 𝐵)

Proof of Theorem sseldi

Step	Hyp	Ref	Expression
1		sseldi.2	. 2 ⊢ (𝜑 → 𝐶 ∈ 𝐴)
2		sseli.1	. . 3 ⊢ 𝐴 ⊆ 𝐵
3	2	sseli 3043	. 2 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)
4	1, 3	syl 14	1 ⊢ (𝜑 → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 1448   ⊆ wss 3021

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-11 1452  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-in 3027  df-ss 3034

This theorem is referenced by:  mptrcl  5435  riotacl  5676  riotasbc  5677  elmpocl  5900  ofrval  5924  f1od2  6062  mpoxopn0yelv  6066  tpostpos  6091  smores  6119  supubti  6801  suplubti  6802  prarloclemcalc  7211  rereceu  7574  recriota  7575  rexrd  7687  eqord1  8112  nnred  8591  nncnd  8592  un0addcl  8862  un0mulcl  8863  nnnn0d  8882  nn0red  8883  nn0xnn0d  8901  suprzclex  9001  nn0zd  9023  zred  9025  rpred  9330  ige2m1fz  9731  zmodfzp1  9962  seq3caopr2  10096  expcl2lemap  10146  m1expcl  10157  summodclem2a  10989  zsumdc  10992  lcmn0cl  11542  ennnfonelemg  11708  lmrcl  12142  lmss  12196  upxp  12222  isxms2  12380  iooretopg  12450  tgqioo  12466  dvcl  12525  dvidlemap  12533  isomninnlem  12809  trilpolemeq1  12817  trilpolemlt1  12818