Theorem sseld 3226

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

Syntax hints:   → wi 4   ∈ wcel 2202   ⊆ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  sselda  3227  sseldd  3228  ssneld  3229  elelpwi  3664  ssbrd  4131  uniopel  4349  onintonm  4615  sucprcreg  4647  ordsuc  4661  0elnn  4717  dmrnssfld  4995  nfunv  5359  opelf  5507  fvimacnv  5762  ffvelcdm  5780  resflem  5811  f1imass  5915  dftpos3  6428  nnmordi  6684  mapsn  6859  ixpf  6889  pw2f1odclem  7020  diffifi  7083  ordiso2  7234  difinfinf  7300  exmidapne  7479  prarloclemarch2  7639  ltexprlemrl  7830  cauappcvgprlemladdrl  7877  caucvgprlemladdrl  7898  caucvgprlem1  7899  axpre-suploclemres  8121  uzind  9591  supinfneg  9829  infsupneg  9830  ixxssxr  10135  elfz0add  10355  fzoss1  10408  elfzoextl  10437  frecuzrdgrclt  10678  ccatval2  11179  swrdswrd  11290  pfxccatin12lem2a  11312  swrdccatin2  11314  pfxccatpfx2  11322  fsum3cvg  11957  isumrpcl  12073  fproddccvg  12151  reumodprminv  12844  issubmnd  13543  issubg2m  13794  eqgid  13831  issubrng2  14243  subrgdvds  14268  issubrg2  14274  lssats2  14447  rnglidlmmgm  14529  rnglidlmsgrp  14530  rnglidlrng  14531  mplbasss  14729  lmtopcnp  14993  txuni2  14999  tx1cn  15012  tx2cn  15013  txlm  15022  imasnopn  15042  xmetunirn  15101  mopnval  15185  metrest  15249  dedekindicc  15376  ivthdec  15387  limcimolemlt  15407  plyssc  15482  edgupgren  16011  subgreldmiedg  16139  clwwlkccatlem  16270  eupth2lemsfi  16348  bj-charfundc  16454  bj-nnord  16604