Theorem elun1 3182

Description: Membership law for union of classes. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
elun1	⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐵 ∪ 𝐶))

Proof of Theorem elun1

Step	Hyp	Ref	Expression
1		ssun1 3178	. 2 ⊢ 𝐵 ⊆ (𝐵 ∪ 𝐶)
2	1	sseli 3035	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐵 ∪ 𝐶))

Syntax hints:   → wi 4   ∈ wcel 1445   ∪ cun 3011

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-v 2635  df-un 3017  df-in 3019  df-ss 3026

This theorem is referenced by:  dcun  3412  exmidundif  4058  exmidundifim  4059  brtposg  6057  dftpos4  6066  dcdifsnid  6303  undifdcss  6713  fidcenumlemrks  6742  djulclr  6821  djulcl  6823  djuss  6841  finomni  6883  hashennnuni  10318  sumsplitdc  10990  srngbased  11781  srngplusgd  11782  srngmulrd  11783  lmodbased  11792  lmodplusgd  11793  lmodscad  11794  ipsbased  11800  ipsaddgd  11801  ipsmulrd  11802