Theorem elun1 3314

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

Assertion

Ref	Expression
elun1	|- ( A e. B -> A e. ( B u. C ) )

Proof of Theorem elun1

Step	Hyp	Ref	Expression
1		ssun1 3310	. 2 |- B C_ ( B u. C )
2	1	sseli 3163	1 |- ( A e. B -> A e. ( B u. C ) )

Syntax hints:   -> wi 4   e. wcel 2158   u. cun 3139

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-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-v 2751  df-un 3145  df-in 3147  df-ss 3154

This theorem is referenced by:  dcun  3545  exmidundif  4218  exmidundifim  4219  brtposg  6269  dftpos4  6278  dcdifsnid  6519  undifdcss  6936  fidcenumlemrks  6966  djulclr  7062  djulcl  7064  djuss  7083  finomni  7152  hashennnuni  10773  sumsplitdc  11454  srngbased  12620  srngplusgd  12621  srngmulrd  12622  lmodbased  12638  lmodplusgd  12639  lmodscad  12640  ipsbased  12650  ipsaddgd  12651  ipsmulrd  12652