Theorem sseld 3196

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

Syntax hints:   → wi 4   ∈ wcel 2177   ⊆ wss 3170

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3176  df-ss 3183

This theorem is referenced by:  sselda  3197  sseldd  3198  ssneld  3199  elelpwi  3633  ssbrd  4094  uniopel  4309  onintonm  4573  sucprcreg  4605  ordsuc  4619  0elnn  4675  dmrnssfld  4950  nfunv  5313  opelf  5458  fvimacnv  5708  ffvelcdm  5726  resflem  5757  f1imass  5856  dftpos3  6361  nnmordi  6615  mapsn  6790  ixpf  6820  pw2f1odclem  6946  diffifi  7006  ordiso2  7152  difinfinf  7218  exmidapne  7392  prarloclemarch2  7552  ltexprlemrl  7743  cauappcvgprlemladdrl  7790  caucvgprlemladdrl  7811  caucvgprlem1  7812  axpre-suploclemres  8034  uzind  9504  supinfneg  9736  infsupneg  9737  ixxssxr  10042  elfz0add  10262  fzoss1  10315  elfzoextl  10342  frecuzrdgrclt  10582  ccatval2  11077  swrdswrd  11181  fsum3cvg  11764  isumrpcl  11880  fproddccvg  11958  reumodprminv  12651  issubmnd  13349  issubg2m  13600  eqgid  13637  issubrng2  14047  subrgdvds  14072  issubrg2  14078  lssats2  14251  rnglidlmmgm  14333  rnglidlmsgrp  14334  rnglidlrng  14335  mplbasss  14533  lmtopcnp  14797  txuni2  14803  tx1cn  14816  tx2cn  14817  txlm  14826  imasnopn  14846  xmetunirn  14905  mopnval  14989  metrest  15053  dedekindicc  15180  ivthdec  15191  limcimolemlt  15211  plyssc  15286  bj-charfundc  15882  bj-nnord  16032