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  6537  nnmordi  6793  mapsnd  6974  mapsn  6976  ixpf  7006  pw2f1odclem  7138  diffifi  7202  ordiso2  7381  difinfinf  7447  exmidapne  7632  prarloclemarch2  7792  ltexprlemrl  7983  cauappcvgprlemladdrl  8030  caucvgprlemladdrl  8051  caucvgprlem1  8052  axpre-suploclemres  8274  uzind  9768  supinfneg  10011  infsupneg  10012  ixxssxr  10319  elfz0add  10544  fzoss1  10597  elfzoextl  10626  frecuzrdgrclt  10873  ccatval2  11388  swrdswrd  11499  pfxccatin12lem2a  11521  swrdccatin2  11523  pfxccatpfx2  11531  fsum3cvg  12170  isumrpcl  12286  fproddccvg  12364  reumodprminv  13061  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemimin  13307  issubmnd  13814  issubg2m  14051  eqgid  14088  issubrng2  14627  subrgdvds  14652  issubrg2  14658  lssats2  14860  rnglidlmmgm  14942  rnglidlmsgrp  14943  rnglidlrng  14944  gsumfsum  15032  issubassa3  15121  mplbasss  15212  lmtopcnp  15476  txuni2  15482  tx1cn  15495  tx2cn  15496  txlm  15505  imasnopn  15525  xmetunirn  15584  mopnval  15668  metrest  15732  dedekindicc  15859  ivthdec  15870  limcimolemlt  15890  plyssc  15965  edgupgren  16587  subgreldmiedg  16715  clwwlkccatlem  16846  eupth2lemsfi  16924  bj-charfundc  17039  bj-nnord  17189