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

Theorem elun2 3475
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 3471 . 2  |-  B  C_  ( C  u.  B
)
21sseli 3304 1  |-  ( A  e.  B  ->  A  e.  ( C  u.  B
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721    u. cun 3278
This theorem is referenced by:  dftpos4  6457  tfrlem11  6608  cantnfp1lem1  7590  cantnfp1lem3  7592  tc2  7637  rankunb  7732  rankelun  7754  dfac2  7967  cfsmolem  8106  isfin4-3  8151  zornn0g  8341  mnfxr  10670  supxrun  10850  sumsplit  12507  prmreclem5  13243  acsfiindd  14558  lspsolv  16170  mplcoe1  16483  restntr  17200  1stckgenlem  17538  fbun  17825  filuni  17870  ufileu  17904  alexsubALTlem4  18034  tmdgsum  18078  icccmplem2  18807  aannenlem2  20199  aalioulem2  20203  wfrlem14  25483  altxpsspw  25726  mbfresfi  26152  itg2addnclem2  26156  sucidVD  28693  bnj553  28975  bnj966  29021  bnj1442  29124  hdmaplem2N  32255  hdmaplem3  32256
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-un 3285  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator