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  4174  uniopel  4399  onintonm  4666  sucprcreg  4698  ordsuc  4712  0elnn  4768  dmrnssfld  5047  nfunv  5413  opelf  5563  fvimacnv  5827  ffvelcdm  5844  resflem  5875  f1imass  5983  suppssrst  6505  suppssrgst  6506  dftpos3  6538  nnmordi  6794  mapsnd  6976  mapsn  6978  ixpf  7008  pw2f1odclem  7140  diffifi  7204  ordiso2  7381  difinfinf  7447  exmidapne  7632  prarloclemarch2  7792  ltexprlemrl  7983  cauappcvgprlemladdrl  8030  caucvgprlemladdrl  8051  caucvgprlem1  8052  axpre-suploclemres  8274  uzind  9767  supinfneg  10010  infsupneg  10011  ixxssxr  10318  elfz0add  10543  fzoss1  10596  elfzoextl  10625  frecuzrdgrclt  10872  ccatval2  11387  swrdswrd  11498  pfxccatin12lem2a  11520  swrdccatin2  11522  pfxccatpfx2  11530  fsum3cvg  12169  isumrpcl  12285  fproddccvg  12363  reumodprminv  13060  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemimin  13306  issubmnd  13813  issubg2m  14050  eqgid  14087  issubrng2  14626  subrgdvds  14651  issubrg2  14657  lssats2  14859  rnglidlmmgm  14941  rnglidlmsgrp  14942  rnglidlrng  14943  gsumfsum  15031  issubassa3  15120  lmtopcnp  15493  txuni2  15499  tx1cn  15512  tx2cn  15513  txlm  15522  imasnopn  15542  xmetunirn  15601  mopnval  15685  metrest  15749  dedekindicc  15876  ivthdec  15887  limcimolemlt  15907  plyssc  15982  edgupgren  16604  subgreldmiedg  16732  clwwlkccatlem  16863  eupth2lemsfi  16941  bj-charfundc  17056  bj-nnord  17206