Theorem sseld 3168

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

Syntax hints:   → wi 4   ∈ wcel 2159   ⊆ wss 3143

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-11 1516  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2170

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-clab 2175  df-cleq 2181  df-clel 2184  df-in 3149  df-ss 3156

This theorem is referenced by:  sselda  3169  sseldd  3170  ssneld  3171  elelpwi  3601  ssbrd  4060  uniopel  4270  onintonm  4530  sucprcreg  4562  ordsuc  4576  0elnn  4632  dmrnssfld  4904  nfunv  5263  opelf  5401  fvimacnv  5646  ffvelcdm  5664  resflem  5695  f1imass  5790  dftpos3  6280  nnmordi  6534  mapsn  6707  ixpf  6737  diffifi  6911  ordiso2  7051  difinfinf  7117  exmidapne  7276  prarloclemarch2  7435  ltexprlemrl  7626  cauappcvgprlemladdrl  7673  caucvgprlemladdrl  7694  caucvgprlem1  7695  axpre-suploclemres  7917  uzind  9381  supinfneg  9612  infsupneg  9613  ixxssxr  9917  elfz0add  10137  fzoss1  10188  frecuzrdgrclt  10432  fsum3cvg  11403  isumrpcl  11519  fproddccvg  11597  reumodprminv  12270  issubmnd  12868  issubg2m  13093  eqgid  13130  issubrng2  13517  subrgdvds  13542  issubrg2  13548  lssats2  13690  rnglidlmmgm  13772  rnglidlmsgrp  13773  rnglidlrng  13774  lmtopcnp  14133  txuni2  14139  tx1cn  14152  tx2cn  14153  txlm  14162  imasnopn  14182  xmetunirn  14241  mopnval  14325  metrest  14389  dedekindicc  14494  ivthdec  14505  limcimolemlt  14516  bj-charfundc  14943  bj-nnord  15093