Theorem sseld 3155

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

Syntax hints:   → wi 4   ∈ wcel 2148   ⊆ wss 3130

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3136  df-ss 3143

This theorem is referenced by:  sselda  3156  sseldd  3157  ssneld  3158  elelpwi  3588  ssbrd  4047  uniopel  4257  onintonm  4517  sucprcreg  4549  ordsuc  4563  0elnn  4619  dmrnssfld  4891  nfunv  5250  opelf  5388  fvimacnv  5632  ffvelcdm  5650  resflem  5681  f1imass  5775  dftpos3  6263  nnmordi  6517  mapsn  6690  ixpf  6720  diffifi  6894  ordiso2  7034  difinfinf  7100  exmidapne  7259  prarloclemarch2  7418  ltexprlemrl  7609  cauappcvgprlemladdrl  7656  caucvgprlemladdrl  7677  caucvgprlem1  7678  axpre-suploclemres  7900  uzind  9364  supinfneg  9595  infsupneg  9596  ixxssxr  9900  elfz0add  10120  fzoss1  10171  frecuzrdgrclt  10415  fsum3cvg  11386  isumrpcl  11502  fproddccvg  11580  reumodprminv  12253  issubmnd  12843  issubg2m  13049  eqgid  13085  subrgdvds  13356  issubrg2  13362  lmtopcnp  13753  txuni2  13759  tx1cn  13772  tx2cn  13773  txlm  13782  imasnopn  13802  xmetunirn  13861  mopnval  13945  metrest  14009  dedekindicc  14114  ivthdec  14125  limcimolemlt  14136  bj-charfundc  14563  bj-nnord  14713