Theorem sseld 3241

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

Syntax hints:   → wi 4   ∈ wcel 2205   ⊆ wss 3214

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  sselda  3242  sseldd  3243  ssneld  3244  elelpwi  3687  ssbrd  4158  uniopel  4379  onintonm  4645  sucprcreg  4677  ordsuc  4691  0elnn  4747  dmrnssfld  5026  nfunv  5391  opelf  5541  fvimacnv  5799  ffvelcdm  5816  resflem  5847  f1imass  5954  suppssrst  6475  suppssrgst  6476  dftpos3  6507  nnmordi  6763  mapsnd  6937  mapsn  6939  ixpf  6969  pw2f1odclem  7101  diffifi  7165  ordiso2  7340  difinfinf  7406  exmidapne  7591  prarloclemarch2  7751  ltexprlemrl  7942  cauappcvgprlemladdrl  7989  caucvgprlemladdrl  8010  caucvgprlem1  8011  axpre-suploclemres  8233  uzind  9711  supinfneg  9949  infsupneg  9950  ixxssxr  10256  elfz0add  10480  fzoss1  10533  elfzoextl  10562  frecuzrdgrclt  10805  ccatval2  11315  swrdswrd  11426  pfxccatin12lem2a  11448  swrdccatin2  11450  pfxccatpfx2  11458  fsum3cvg  12094  isumrpcl  12210  fproddccvg  12288  reumodprminv  12981  ballotfilemfc0  13181  ballotfilemfcc  13182  ballotfilemimin  13198  issubmnd  13708  issubg2m  13947  eqgid  13984  issubrng2  14461  subrgdvds  14486  issubrg2  14492  lssats2  14693  rnglidlmmgm  14775  rnglidlmsgrp  14776  rnglidlrng  14777  mplbasss  14982  lmtopcnp  15246  txuni2  15252  tx1cn  15265  tx2cn  15266  txlm  15275  imasnopn  15295  xmetunirn  15354  mopnval  15438  metrest  15502  dedekindicc  15629  ivthdec  15640  limcimolemlt  15660  plyssc  15735  edgupgren  16267  subgreldmiedg  16395  clwwlkccatlem  16526  eupth2lemsfi  16604  bj-charfundc  16719  bj-nnord  16869