Theorem sseld 3038

Description: Membership deduction from subclass relationship. (Contributed by NM, 15-Nov-1995.)

Hypothesis

Ref	Expression
sseld.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Assertion

Ref	Expression
sseld	⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))

Proof of Theorem sseld

Step	Hyp	Ref	Expression
1		sseld.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		ssel 3033	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ∈ wcel 1445   ⊆ wss 3013

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 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-11 1449  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-in 3019  df-ss 3026

This theorem is referenced by:  sselda  3039  sseldd  3040  ssneld  3041  elelpwi  3461  ssbrd  3908  uniopel  4107  onintonm  4362  sucprcreg  4393  ordsuc  4407  0elnn  4460  dmrnssfld  4728  nfunv  5081  opelf  5217  fvimacnv  5453  ffvelrn  5471  resflem  5501  f1imass  5591  dftpos3  6065  nnmordi  6315  mapsn  6487  ixpf  6517  diffifi  6690  ordiso2  6808  prarloclemarch2  7075  ltexprlemrl  7266  cauappcvgprlemladdrl  7313  caucvgprlemladdrl  7334  caucvgprlem1  7335  uzind  8956  supinfneg  9182  infsupneg  9183  ixxssxr  9466  elfz0add  9683  fzoss1  9731  frecuzrdgrclt  9971  fsum3cvg  10936  isumrpcl  11053  lmtopcnp  12117  xmetunirn  12160  mopnval  12244  metrest  12308  bj-nnord  12577