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  7376  difinfinf  7442  exmidapne  7627  prarloclemarch2  7787  ltexprlemrl  7978  cauappcvgprlemladdrl  8025  caucvgprlemladdrl  8046  caucvgprlem1  8047  axpre-suploclemres  8269  uzind  9762  supinfneg  10005  infsupneg  10006  ixxssxr  10313  elfz0add  10538  fzoss1  10591  elfzoextl  10620  frecuzrdgrclt  10867  ccatval2  11382  swrdswrd  11493  pfxccatin12lem2a  11515  swrdccatin2  11517  pfxccatpfx2  11525  fsum3cvg  12164  isumrpcl  12280  fproddccvg  12358  reumodprminv  13055  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemimin  13301  issubmnd  13808  issubg2m  14045  eqgid  14082  issubrng2  14602  subrgdvds  14627  issubrg2  14633  lssats2  14835  rnglidlmmgm  14917  rnglidlmsgrp  14918  rnglidlrng  14919  gsumfsum  15007  issubassa3  15096  mplbasss  15178  lmtopcnp  15442  txuni2  15448  tx1cn  15461  tx2cn  15462  txlm  15471  imasnopn  15491  xmetunirn  15550  mopnval  15634  metrest  15698  dedekindicc  15825  ivthdec  15836  limcimolemlt  15856  plyssc  15931  edgupgren  16548  subgreldmiedg  16676  clwwlkccatlem  16807  eupth2lemsfi  16885  bj-charfundc  17000  bj-nnord  17150