Theorem sseld 3182

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

Syntax hints:   → wi 4   ∈ wcel 2167   ⊆ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  sselda  3183  sseldd  3184  ssneld  3185  elelpwi  3617  ssbrd  4076  uniopel  4289  onintonm  4553  sucprcreg  4585  ordsuc  4599  0elnn  4655  dmrnssfld  4929  nfunv  5291  opelf  5429  fvimacnv  5677  ffvelcdm  5695  resflem  5726  f1imass  5821  dftpos3  6320  nnmordi  6574  mapsn  6749  ixpf  6779  pw2f1odclem  6895  diffifi  6955  ordiso2  7101  difinfinf  7167  exmidapne  7327  prarloclemarch2  7486  ltexprlemrl  7677  cauappcvgprlemladdrl  7724  caucvgprlemladdrl  7745  caucvgprlem1  7746  axpre-suploclemres  7968  uzind  9437  supinfneg  9669  infsupneg  9670  ixxssxr  9975  elfz0add  10195  fzoss1  10247  frecuzrdgrclt  10507  fsum3cvg  11543  isumrpcl  11659  fproddccvg  11737  reumodprminv  12422  issubmnd  13083  issubg2m  13319  eqgid  13356  issubrng2  13766  subrgdvds  13791  issubrg2  13797  lssats2  13970  rnglidlmmgm  14052  rnglidlmsgrp  14053  rnglidlrng  14054  lmtopcnp  14486  txuni2  14492  tx1cn  14505  tx2cn  14506  txlm  14515  imasnopn  14535  xmetunirn  14594  mopnval  14678  metrest  14742  dedekindicc  14869  ivthdec  14880  limcimolemlt  14900  plyssc  14975  bj-charfundc  15454  bj-nnord  15604