Theorem elun1 3569

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

Syntax hints:   -> wi 4   e. wcel 1891   u. cun 3370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-v 3015  df-un 3377  df-in 3379  df-ss 3386

This theorem is referenced by:  brtpos  6969  dftpos4  6979  domunsncan  7659  unxpdomlem2  7764  rankunb  8308  rankelun  8330  fin1a2lem10  8826  zornn0g  8922  xrsupexmnf  11580  xrinfmexpnf  11581  sumsplit  13840  lcmfunsnlem2lem1  14622  lcmfunsnlem2  14624  prmreclem5  14875  lbsextlem3  18394  restntr  20209  comppfsc  20558  1stckgenlem  20579  fbun  20866  filcon  20909  filuni  20911  alexsubALTlem4  21076  ovolfiniun  22465  volfiniun  22512  elplyd  23168  ply1term  23170  aannenlem2  23297  aalioulem2  23301  eengbas  25023  ecgrtg  25025  vdgrf  25638  gsumle  28549  bnj1498  29876  mrsubcn  30163  mrsubco  30165  altxpsspw  30750  poimirlem9  31951  poimirlem22  31964  poimirlem31  31973  poimirlem32  31974  mbfresfi  31989  itg2addnclem2  31996  ftc1anclem7  32025  ftc1anc  32027  hdmaplem1  35341  hdmap1eulem  35394  sucidALTVD  37264  sucidALT  37265  founiiun0  37475  mccllem  37719  limcresiooub  37765  limcresioolb  37766  dvmptfprodlem  37861  dvnprodlem2  37864  fourierdlem48  38075  fourierdlem49  38076  fourierdlem51  38078  fourierdlem54  38081  fourierdlem62  38089  fourierdlem71  38098  fourierdlem103  38130  fourierdlem104  38131  fourierdlem114  38141  fouriersw  38152  nnfoctbdjlem  38354  hoidmvlelem2  38481  hoidmvlelem3  38482