Theorem ssel2 3174

Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 7-Jun-2004.)

Assertion

Ref	Expression
ssel2	⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵)

Proof of Theorem ssel2

Step	Hyp	Ref	Expression
1		ssel 3173	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
2	1	imp 124	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2164   ⊆ wss 3153

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 3159  df-ss 3166

This theorem is referenced by:  elnn  4638  funimass4  5607  fvelimab  5613  ssimaex  5618  funconstss  5676  rexima  5797  ralima  5798  1st2nd  6234  f1o2ndf1  6281  tfri1dALT  6404  eldju1st  7130  axsuploc  8092  lbinf  8967  dfinfre  8975  lbzbi  9681  elfzom1elp1fzo  10269  ssfzo12  10291  seq3split  10559  seqsplitg  10560  shftlem  10960  uzwodc  12174  subgintm  13268  subrngintm  13708  subrgintm  13739  tgcl  14232  neipsm  14322  txbasval  14435  elmopn2  14617  metrest  14674  cncfmet  14747  negcncf  14759  ply1term  14889  plyconst  14891  reeff1olem  14906