Theorem sseld 3191

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

Syntax hints:   → wi 4   ∈ wcel 2175   ⊆ wss 3165

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-in 3171  df-ss 3178

This theorem is referenced by:  sselda  3192  sseldd  3193  ssneld  3194  elelpwi  3627  ssbrd  4086  uniopel  4299  onintonm  4563  sucprcreg  4595  ordsuc  4609  0elnn  4665  dmrnssfld  4939  nfunv  5301  opelf  5441  fvimacnv  5689  ffvelcdm  5707  resflem  5738  f1imass  5833  dftpos3  6338  nnmordi  6592  mapsn  6767  ixpf  6797  pw2f1odclem  6913  diffifi  6973  ordiso2  7119  difinfinf  7185  exmidapne  7354  prarloclemarch2  7514  ltexprlemrl  7705  cauappcvgprlemladdrl  7752  caucvgprlemladdrl  7773  caucvgprlem1  7774  axpre-suploclemres  7996  uzind  9466  supinfneg  9698  infsupneg  9699  ixxssxr  10004  elfz0add  10224  fzoss1  10276  elfzoextl  10301  frecuzrdgrclt  10541  ccatval2  11029  fsum3cvg  11608  isumrpcl  11724  fproddccvg  11802  reumodprminv  12495  issubmnd  13192  issubg2m  13443  eqgid  13480  issubrng2  13890  subrgdvds  13915  issubrg2  13921  lssats2  14094  rnglidlmmgm  14176  rnglidlmsgrp  14177  rnglidlrng  14178  mplbasss  14376  lmtopcnp  14640  txuni2  14646  tx1cn  14659  tx2cn  14660  txlm  14669  imasnopn  14689  xmetunirn  14748  mopnval  14832  metrest  14896  dedekindicc  15023  ivthdec  15034  limcimolemlt  15054  plyssc  15129  bj-charfundc  15608  bj-nnord  15758