Theorem elun1 3474

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

Syntax hints:   -> wi 4   e. wcel 1721   u. cun 3278

This theorem is referenced by:  brtpos  6447  dftpos4  6457  domunsncan  7167  unxpdomlem2  7273  rankunb  7732  rankelun  7754  fin1a2lem10  8245  zornn0g  8341  xrsupexmnf  10839  xrinfmexpnf  10840  sumsplit  12507  prmreclem5  13243  lbsextlem3  16187  restntr  17200  1stckgenlem  17538  fbun  17825  filcon  17868  filuni  17870  alexsubALTlem4  18034  ovolfiniun  19350  volfiniun  19394  elplyd  20074  ply1term  20076  aannenlem2  20199  aalioulem2  20203  vdgrf  21622  altxpsspw  25726  mbfresfi  26152  itg2addnclem2  26156  comppfsc  26277  sucidALTVD  28691  sucidALT  28692  bnj1498  29136  hdmaplem1  32254  hdmap1eulem  32307

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-un 3285  df-in 3287  df-ss 3294