Theorem sseld 3223

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

Syntax hints:   → wi 4   ∈ wcel 2200   ⊆ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  sselda  3224  sseldd  3225  ssneld  3226  elelpwi  3661  ssbrd  4125  uniopel  4342  onintonm  4608  sucprcreg  4640  ordsuc  4654  0elnn  4710  dmrnssfld  4986  nfunv  5350  opelf  5495  fvimacnv  5749  ffvelcdm  5767  resflem  5798  f1imass  5897  dftpos3  6406  nnmordi  6660  mapsn  6835  ixpf  6865  pw2f1odclem  6991  diffifi  7052  ordiso2  7198  difinfinf  7264  exmidapne  7442  prarloclemarch2  7602  ltexprlemrl  7793  cauappcvgprlemladdrl  7840  caucvgprlemladdrl  7861  caucvgprlem1  7862  axpre-suploclemres  8084  uzind  9554  supinfneg  9786  infsupneg  9787  ixxssxr  10092  elfz0add  10312  fzoss1  10365  elfzoextl  10392  frecuzrdgrclt  10632  ccatval2  11128  swrdswrd  11232  pfxccatin12lem2a  11254  swrdccatin2  11256  pfxccatpfx2  11264  fsum3cvg  11884  isumrpcl  12000  fproddccvg  12078  reumodprminv  12771  issubmnd  13470  issubg2m  13721  eqgid  13758  issubrng2  14168  subrgdvds  14193  issubrg2  14199  lssats2  14372  rnglidlmmgm  14454  rnglidlmsgrp  14455  rnglidlrng  14456  mplbasss  14654  lmtopcnp  14918  txuni2  14924  tx1cn  14937  tx2cn  14938  txlm  14947  imasnopn  14967  xmetunirn  15026  mopnval  15110  metrest  15174  dedekindicc  15301  ivthdec  15312  limcimolemlt  15332  plyssc  15407  edgupgren  15933  bj-charfundc  16129  bj-nnord  16279