Theorem sseld 3179

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

Syntax hints:   → wi 4   ∈ wcel 2164   ⊆ wss 3154

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167

This theorem is referenced by:  sselda  3180  sseldd  3181  ssneld  3182  elelpwi  3614  ssbrd  4073  uniopel  4286  onintonm  4550  sucprcreg  4582  ordsuc  4596  0elnn  4652  dmrnssfld  4926  nfunv  5288  opelf  5426  fvimacnv  5674  ffvelcdm  5692  resflem  5723  f1imass  5818  dftpos3  6317  nnmordi  6571  mapsn  6746  ixpf  6776  pw2f1odclem  6892  diffifi  6952  ordiso2  7096  difinfinf  7162  exmidapne  7322  prarloclemarch2  7481  ltexprlemrl  7672  cauappcvgprlemladdrl  7719  caucvgprlemladdrl  7740  caucvgprlem1  7741  axpre-suploclemres  7963  uzind  9431  supinfneg  9663  infsupneg  9664  ixxssxr  9969  elfz0add  10189  fzoss1  10241  frecuzrdgrclt  10489  fsum3cvg  11524  isumrpcl  11640  fproddccvg  11718  reumodprminv  12394  issubmnd  13026  issubg2m  13262  eqgid  13299  issubrng2  13709  subrgdvds  13734  issubrg2  13740  lssats2  13913  rnglidlmmgm  13995  rnglidlmsgrp  13996  rnglidlrng  13997  lmtopcnp  14429  txuni2  14435  tx1cn  14448  tx2cn  14449  txlm  14458  imasnopn  14478  xmetunirn  14537  mopnval  14621  metrest  14685  dedekindicc  14812  ivthdec  14823  limcimolemlt  14843  plyssc  14918  bj-charfundc  15370  bj-nnord  15520