Theorem sseld 3224

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

Syntax hints:   → wi 4   ∈ wcel 2200   ⊆ wss 3198

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211

This theorem is referenced by:  sselda  3225  sseldd  3226  ssneld  3227  elelpwi  3662  ssbrd  4129  uniopel  4347  onintonm  4613  sucprcreg  4645  ordsuc  4659  0elnn  4715  dmrnssfld  4993  nfunv  5357  opelf  5504  fvimacnv  5758  ffvelcdm  5776  resflem  5807  f1imass  5910  dftpos3  6423  nnmordi  6679  mapsn  6854  ixpf  6884  pw2f1odclem  7015  diffifi  7076  ordiso2  7225  difinfinf  7291  exmidapne  7469  prarloclemarch2  7629  ltexprlemrl  7820  cauappcvgprlemladdrl  7867  caucvgprlemladdrl  7888  caucvgprlem1  7889  axpre-suploclemres  8111  uzind  9581  supinfneg  9819  infsupneg  9820  ixxssxr  10125  elfz0add  10345  fzoss1  10398  elfzoextl  10426  frecuzrdgrclt  10667  ccatval2  11165  swrdswrd  11276  pfxccatin12lem2a  11298  swrdccatin2  11300  pfxccatpfx2  11308  fsum3cvg  11929  isumrpcl  12045  fproddccvg  12123  reumodprminv  12816  issubmnd  13515  issubg2m  13766  eqgid  13803  issubrng2  14214  subrgdvds  14239  issubrg2  14245  lssats2  14418  rnglidlmmgm  14500  rnglidlmsgrp  14501  rnglidlrng  14502  mplbasss  14700  lmtopcnp  14964  txuni2  14970  tx1cn  14983  tx2cn  14984  txlm  14993  imasnopn  15013  xmetunirn  15072  mopnval  15156  metrest  15220  dedekindicc  15347  ivthdec  15358  limcimolemlt  15378  plyssc  15453  edgupgren  15980  clwwlkccatlem  16195  bj-charfundc  16339  bj-nnord  16489