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 ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ∈ wcel 2209   ⊆ wss 3220

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 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 theorem 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 referenced by:  sselda  3248  sseldd  3249  ssneld  3250  elelpwi  3697  ssbrd  4168  uniopel  4392  onintonm  4659  sucprcreg  4691  ordsuc  4705  0elnn  4761  dmrnssfld  5040  nfunv  5405  opelf  5555  fvimacnv  5815  ffvelcdm  5832  resflem  5863  f1imass  5970  suppssrst  6491  suppssrgst  6492  dftpos3  6523  nnmordi  6779  mapsnd  6960  mapsn  6962  ixpf  6992  pw2f1odclem  7124  diffifi  7188  ordiso2  7365  difinfinf  7431  exmidapne  7616  prarloclemarch2  7776  ltexprlemrl  7967  cauappcvgprlemladdrl  8014  caucvgprlemladdrl  8035  caucvgprlem1  8036  axpre-suploclemres  8258  uzind  9736  supinfneg  9974  infsupneg  9975  ixxssxr  10281  elfz0add  10505  fzoss1  10558  elfzoextl  10587  frecuzrdgrclt  10830  ccatval2  11344  swrdswrd  11455  pfxccatin12lem2a  11477  swrdccatin2  11479  pfxccatpfx2  11487  fsum3cvg  12123  isumrpcl  12239  fproddccvg  12317  reumodprminv  13010  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemimin  13227  issubmnd  13732  issubg2m  13969  eqgid  14006  issubrng2  14491  subrgdvds  14516  issubrg2  14522  lssats2  14723  rnglidlmmgm  14805  rnglidlmsgrp  14806  rnglidlrng  14807  gsumfsum  14895  mplbasss  15010  lmtopcnp  15274  txuni2  15280  tx1cn  15293  tx2cn  15294  txlm  15303  imasnopn  15323  xmetunirn  15382  mopnval  15466  metrest  15530  dedekindicc  15657  ivthdec  15668  limcimolemlt  15688  plyssc  15763  edgupgren  16296  subgreldmiedg  16424  clwwlkccatlem  16555  eupth2lemsfi  16633  bj-charfundc  16748  bj-nnord  16898