MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elun1 Structured version   Unicode version

Theorem elun1 3516
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
StepHypRef Expression
1 ssun1 3512 . 2  |-  B  C_  ( B  u.  C
)
21sseli 3346 1  |-  ( A  e.  B  ->  A  e.  ( B  u.  C
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726    u. cun 3320
This theorem is referenced by:  brtpos  6491  dftpos4  6501  domunsncan  7211  unxpdomlem2  7317  rankunb  7779  rankelun  7801  fin1a2lem10  8294  zornn0g  8390  xrsupexmnf  10888  xrinfmexpnf  10889  sumsplit  12557  prmreclem5  13293  lbsextlem3  16237  restntr  17251  1stckgenlem  17590  fbun  17877  filcon  17920  filuni  17922  alexsubALTlem4  18086  ovolfiniun  19402  volfiniun  19446  elplyd  20126  ply1term  20128  aannenlem2  20251  aalioulem2  20255  vdgrf  21674  altxpsspw  25827  mbfresfi  26265  itg2addnclem2  26271  ftc1anclem7  26300  ftc1anc  26302  comppfsc  26401  sucidALTVD  29056  sucidALT  29057  bnj1498  29504  hdmaplem1  32643  hdmap1eulem  32696
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-un 3327  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator