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

Theorem elun2 3343
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 3339 . 2  |-  B  C_  ( C  u.  B
)
21sseli 3176 1  |-  ( A  e.  B  ->  A  e.  ( C  u.  B
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684    u. cun 3150
This theorem is referenced by:  dftpos4  6253  tfrlem11  6404  cantnfp1lem1  7380  cantnfp1lem3  7382  tc2  7427  rankunb  7522  rankelun  7544  dfac2  7757  cfsmolem  7896  isfin4-3  7941  zornn0g  8132  mnfxr  10456  supxrun  10634  sumsplit  12231  prmreclem5  12967  acsfiindd  14280  lspsolv  15896  mplcoe1  16209  restntr  16912  1stckgenlem  17248  fbun  17535  filuni  17580  ufileu  17614  alexsubALTlem4  17744  tmdgsum  17778  icccmplem2  18328  aannenlem2  19709  aalioulem2  19713  wfrlem14  24269  altxpsspw  24511  sucidVD  28648  bnj553  28930  bnj966  28976  bnj1442  29079  hdmaplem2N  31962  hdmaplem3  31963
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator