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  5914  dftpos3  6427  nnmordi  6683  mapsn  6858  ixpf  6888  pw2f1odclem  7019  diffifi  7082  ordiso2  7233  difinfinf  7299  exmidapne  7478  prarloclemarch2  7638  ltexprlemrl  7829  cauappcvgprlemladdrl  7876  caucvgprlemladdrl  7897  caucvgprlem1  7898  axpre-suploclemres  8120  uzind  9590  supinfneg  9828  infsupneg  9829  ixxssxr  10134  elfz0add  10354  fzoss1  10407  elfzoextl  10435  frecuzrdgrclt  10676  ccatval2  11174  swrdswrd  11285  pfxccatin12lem2a  11307  swrdccatin2  11309  pfxccatpfx2  11317  fsum3cvg  11938  isumrpcl  12054  fproddccvg  12132  reumodprminv  12825  issubmnd  13524  issubg2m  13775  eqgid  13812  issubrng2  14223  subrgdvds  14248  issubrg2  14254  lssats2  14427  rnglidlmmgm  14509  rnglidlmsgrp  14510  rnglidlrng  14511  mplbasss  14709  lmtopcnp  14973  txuni2  14979  tx1cn  14992  tx2cn  14993  txlm  15002  imasnopn  15022  xmetunirn  15081  mopnval  15165  metrest  15229  dedekindicc  15356  ivthdec  15367  limcimolemlt  15387  plyssc  15462  edgupgren  15991  subgreldmiedg  16119  clwwlkccatlem  16250  bj-charfundc  16403  bj-nnord  16553