Theorem elun1 3626

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 3622	. 2 |- B C_ ( B u. C )
2	1	sseli 3455	1 |- ( A e. B -> A e. ( B u. C ) )

Syntax hints:   -> wi 4   e. wcel 1758   u. cun 3429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954  ax-ext 2431

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-v 3074  df-un 3436  df-in 3438  df-ss 3445

This theorem is referenced by:  brtpos  6859  dftpos4  6869  domunsncan  7516  unxpdomlem2  7624  rankunb  8163  rankelun  8185  fin1a2lem10  8684  zornn0g  8780  xrsupexmnf  11373  xrinfmexpnf  11374  sumsplit  13348  prmreclem5  14094  lbsextlem3  17359  restntr  18913  1stckgenlem  19253  fbun  19540  filcon  19583  filuni  19585  alexsubALTlem4  19749  ovolfiniun  21111  volfiniun  21156  elplyd  21798  ply1term  21800  aannenlem2  21923  aalioulem2  21927  eengbas  23374  ecgrtg  23376  vdgrf  23715  altxpsspw  28147  mbfresfi  28581  itg2addnclem2  28587  ftc1anclem7  28616  ftc1anc  28618  comppfsc  28722  sucidALTVD  31919  sucidALT  31920  bnj1498  32365  hdmaplem1  35735  hdmap1eulem  35788