Theorem sseld 3227

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

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

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 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  sselda  3228  sseldd  3229  ssneld  3230  elelpwi  3668  ssbrd  4136  uniopel  4355  onintonm  4621  sucprcreg  4653  ordsuc  4667  0elnn  4723  dmrnssfld  5001  nfunv  5366  opelf  5515  fvimacnv  5771  ffvelcdm  5788  resflem  5819  f1imass  5925  suppssrst  6439  suppssrgst  6440  dftpos3  6471  nnmordi  6727  mapsn  6902  ixpf  6932  pw2f1odclem  7063  diffifi  7126  ordiso2  7277  difinfinf  7343  exmidapne  7522  prarloclemarch2  7682  ltexprlemrl  7873  cauappcvgprlemladdrl  7920  caucvgprlemladdrl  7941  caucvgprlem1  7942  axpre-suploclemres  8164  uzind  9635  supinfneg  9873  infsupneg  9874  ixxssxr  10179  elfz0add  10400  fzoss1  10453  elfzoextl  10482  frecuzrdgrclt  10723  ccatval2  11224  swrdswrd  11335  pfxccatin12lem2a  11357  swrdccatin2  11359  pfxccatpfx2  11367  fsum3cvg  12002  isumrpcl  12118  fproddccvg  12196  reumodprminv  12889  issubmnd  13588  issubg2m  13839  eqgid  13876  issubrng2  14288  subrgdvds  14313  issubrg2  14319  lssats2  14493  rnglidlmmgm  14575  rnglidlmsgrp  14576  rnglidlrng  14577  mplbasss  14780  lmtopcnp  15044  txuni2  15050  tx1cn  15063  tx2cn  15064  txlm  15073  imasnopn  15093  xmetunirn  15152  mopnval  15236  metrest  15300  dedekindicc  15427  ivthdec  15438  limcimolemlt  15458  plyssc  15533  edgupgren  16065  subgreldmiedg  16193  clwwlkccatlem  16324  eupth2lemsfi  16402  bj-charfundc  16507  bj-nnord  16657