Theorem sseld 3237

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

Syntax hints:   → wi 4   ∈ wcel 2203   ⊆ wss 3211

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 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3217  df-ss 3224

This theorem is referenced by:  sselda  3238  sseldd  3239  ssneld  3240  elelpwi  3681  ssbrd  4152  uniopel  4373  onintonm  4639  sucprcreg  4671  ordsuc  4685  0elnn  4741  dmrnssfld  5020  nfunv  5385  opelf  5535  fvimacnv  5793  ffvelcdm  5810  resflem  5841  f1imass  5947  suppssrst  6461  suppssrgst  6462  dftpos3  6493  nnmordi  6749  mapsnd  6923  mapsn  6925  ixpf  6955  pw2f1odclem  7087  diffifi  7151  ordiso2  7326  difinfinf  7392  exmidapne  7574  prarloclemarch2  7734  ltexprlemrl  7925  cauappcvgprlemladdrl  7972  caucvgprlemladdrl  7993  caucvgprlem1  7994  axpre-suploclemres  8216  uzind  9689  supinfneg  9927  infsupneg  9928  ixxssxr  10233  elfz0add  10454  fzoss1  10507  elfzoextl  10536  frecuzrdgrclt  10777  ccatval2  11286  swrdswrd  11397  pfxccatin12lem2a  11419  swrdccatin2  11421  pfxccatpfx2  11429  fsum3cvg  12064  isumrpcl  12180  fproddccvg  12258  reumodprminv  12951  issubmnd  13655  issubg2m  13906  eqgid  13943  issubrng2  14355  subrgdvds  14380  issubrg2  14386  lssats2  14562  rnglidlmmgm  14644  rnglidlmsgrp  14645  rnglidlrng  14646  mplbasss  14851  lmtopcnp  15115  txuni2  15121  tx1cn  15134  tx2cn  15135  txlm  15144  imasnopn  15164  xmetunirn  15223  mopnval  15307  metrest  15371  dedekindicc  15498  ivthdec  15509  limcimolemlt  15529  plyssc  15604  edgupgren  16136  subgreldmiedg  16264  clwwlkccatlem  16395  eupth2lemsfi  16473  bj-charfundc  16578  bj-nnord  16728