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

Theorem elun2 3356
Description: Membership law for union of classes. (Contributed by NM, 30-Aug-1993.)
Assertion
Ref Expression
elun2  |-  ( A  e.  B  ->  A  e.  ( C  u.  B
) )

Proof of Theorem elun2
StepHypRef Expression
1 ssun2 3352 . 2  |-  B  C_  ( C  u.  B
)
21sseli 3189 1  |-  ( A  e.  B  ->  A  e.  ( C  u.  B
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696    u. cun 3163
This theorem is referenced by:  dftpos4  6269  tfrlem11  6420  cantnfp1lem1  7396  cantnfp1lem3  7398  tc2  7443  rankunb  7538  rankelun  7560  dfac2  7773  cfsmolem  7912  isfin4-3  7957  zornn0g  8148  mnfxr  10472  supxrun  10650  sumsplit  12247  prmreclem5  12983  acsfiindd  14296  lspsolv  15912  mplcoe1  16225  restntr  16928  1stckgenlem  17264  fbun  17551  filuni  17596  ufileu  17630  alexsubALTlem4  17760  tmdgsum  17794  icccmplem2  18344  aannenlem2  19725  aalioulem2  19729  wfrlem14  24340  altxpsspw  24583  itg2addnclem2  25004  sucidVD  28964  bnj553  29246  bnj966  29292  bnj1442  29395  hdmaplem2N  32584  hdmaplem3  32585
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator