Theorem sseld 3247

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209   ⊆ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  sselda  3248  sseldd  3249  ssneld  3250  elelpwi  3701  ssbrd  4173  uniopel  4397  onintonm  4664  sucprcreg  4696  ordsuc  4710  0elnn  4766  dmrnssfld  5045  nfunv  5410  opelf  5560  fvimacnv  5824  ffvelcdm  5841  resflem  5872  f1imass  5980  suppssrst  6501  suppssrgst  6502  dftpos3  6533  nnmordi  6789  mapsnd  6970  mapsn  6972  ixpf  7002  pw2f1odclem  7134  diffifi  7198  ordiso2  7375  difinfinf  7441  exmidapne  7626  prarloclemarch2  7786  ltexprlemrl  7977  cauappcvgprlemladdrl  8024  caucvgprlemladdrl  8045  caucvgprlem1  8046  axpre-suploclemres  8268  uzind  9757  supinfneg  9995  infsupneg  9996  ixxssxr  10302  elfz0add  10527  fzoss1  10580  elfzoextl  10609  frecuzrdgrclt  10852  ccatval2  11366  swrdswrd  11477  pfxccatin12lem2a  11499  swrdccatin2  11501  pfxccatpfx2  11509  fsum3cvg  12145  isumrpcl  12261  fproddccvg  12339  reumodprminv  13032  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemimin  13249  issubmnd  13755  issubg2m  13992  eqgid  14029  issubrng2  14518  subrgdvds  14543  issubrg2  14549  lssats2  14751  rnglidlmmgm  14833  rnglidlmsgrp  14834  rnglidlrng  14835  gsumfsum  14923  issubassa3  15012  mplbasss  15087  lmtopcnp  15351  txuni2  15357  tx1cn  15370  tx2cn  15371  txlm  15380  imasnopn  15400  xmetunirn  15459  mopnval  15543  metrest  15607  dedekindicc  15734  ivthdec  15745  limcimolemlt  15765  plyssc  15840  edgupgren  16382  subgreldmiedg  16510  clwwlkccatlem  16641  eupth2lemsfi  16719  bj-charfundc  16834  bj-nnord  16984