Theorem elun1 3657

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

Syntax hints:   -> wi 4   e. wcel 1823   u. cun 3459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-un 3466  df-in 3468  df-ss 3475

This theorem is referenced by:  brtpos  6956  dftpos4  6966  domunsncan  7610  unxpdomlem2  7718  rankunb  8259  rankelun  8281  fin1a2lem10  8780  zornn0g  8876  xrsupexmnf  11499  xrinfmexpnf  11500  sumsplit  13665  prmreclem5  14522  lbsextlem3  18001  restntr  19850  comppfsc  20199  1stckgenlem  20220  fbun  20507  filcon  20550  filuni  20552  alexsubALTlem4  20716  ovolfiniun  22078  volfiniun  22123  elplyd  22765  ply1term  22767  aannenlem2  22891  aalioulem2  22895  eengbas  24486  ecgrtg  24488  vdgrf  25100  gsumle  28004  mrsubcn  29143  mrsubco  29145  altxpsspw  29855  mbfresfi  30301  itg2addnclem2  30307  ftc1anclem7  30336  ftc1anc  30338  mccllem  31844  limcresiooub  31887  limcresioolb  31888  dvmptfprodlem  31980  dvnprodlem2  31983  fourierdlem48  32176  fourierdlem49  32177  fourierdlem51  32179  fourierdlem54  32182  fourierdlem62  32190  fourierdlem71  32199  fourierdlem103  32231  fourierdlem104  32232  fourierdlem114  32242  fouriersw  32253  sucidALTVD  34071  sucidALT  34072  bnj1498  34518  hdmaplem1  37895  hdmap1eulem  37948