Theorem sseld 3146

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

Syntax hints:   → wi 4   ∈ wcel 2141   ⊆ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  sselda  3147  sseldd  3148  ssneld  3149  elelpwi  3578  ssbrd  4032  uniopel  4241  onintonm  4501  sucprcreg  4533  ordsuc  4547  0elnn  4603  dmrnssfld  4874  nfunv  5231  opelf  5369  fvimacnv  5611  ffvelrn  5629  resflem  5660  f1imass  5753  dftpos3  6241  nnmordi  6495  mapsn  6668  ixpf  6698  diffifi  6872  ordiso2  7012  difinfinf  7078  prarloclemarch2  7381  ltexprlemrl  7572  cauappcvgprlemladdrl  7619  caucvgprlemladdrl  7640  caucvgprlem1  7641  axpre-suploclemres  7863  uzind  9323  supinfneg  9554  infsupneg  9555  ixxssxr  9857  elfz0add  10076  fzoss1  10127  frecuzrdgrclt  10371  fsum3cvg  11341  isumrpcl  11457  fproddccvg  11535  reumodprminv  12207  lmtopcnp  13044  txuni2  13050  tx1cn  13063  tx2cn  13064  txlm  13073  imasnopn  13093  xmetunirn  13152  mopnval  13236  metrest  13300  dedekindicc  13405  ivthdec  13416  limcimolemlt  13427  bj-charfundc  13843  bj-nnord  13993