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

Theorem elun1 3418
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 3414 . 2  |-  B  C_  ( B  u.  C
)
21sseli 3252 1  |-  ( A  e.  B  ->  A  e.  ( B  u.  C
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1710    u. cun 3226
This theorem is referenced by:  brtpos  6330  dftpos4  6340  domunsncan  7050  unxpdomlem2  7156  rankunb  7612  rankelun  7634  fin1a2lem10  8125  zornn0g  8222  xrsupexmnf  10715  xrinfmexpnf  10716  sumsplit  12328  prmreclem5  13064  lbsextlem3  16012  restntr  17018  1stckgenlem  17354  fbun  17637  filcon  17680  filuni  17682  alexsubALTlem4  17846  ovolfiniun  18964  volfiniun  19008  elplyd  19688  ply1term  19690  aannenlem2  19813  aalioulem2  19817  altxpsspw  25070  itg2addnclem2  25493  comppfsc  25631  vdgref  27805  sucidALTVD  28408  sucidALT  28409  bnj1498  28853  hdmaplem1  32030  hdmap1eulem  32083
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-v 2866  df-un 3233  df-in 3235  df-ss 3242
  Copyright terms: Public domain W3C validator