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

Theorem elun2 3529
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 3525 . 2  |-  B  C_  ( C  u.  B
)
21sseli 3357 1  |-  ( A  e.  B  ->  A  e.  ( C  u.  B
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756    u. cun 3331
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-v 2979  df-un 3338  df-in 3340  df-ss 3347
This theorem is referenced by:  dftpos4  6769  tfrlem11  6852  findcard2d  7559  cantnfp1lem1  7891  cantnfp1lem3  7893  cantnfp1lem1OLD  7917  cantnfp1lem3OLD  7919  tc2  7967  rankunb  8062  rankelun  8084  dfac2  8305  cfsmolem  8444  isfin4-3  8489  zornn0g  8679  mnfxr  11099  supxrun  11283  sumsplit  13240  prmreclem5  13986  acsfiindd  15352  lspsolv  17229  mplcoe1  17549  maducoeval2  18451  restntr  18791  1stckgenlem  19131  fbun  19418  filuni  19463  ufileu  19497  alexsubALTlem4  19627  tmdgsum  19671  icccmplem2  20405  aannenlem2  21800  aalioulem2  21804  ebtwntg  23233  elntg  23235  wfrlem14  27742  altxpsspw  28013  mbfresfi  28443  itg2addnclem2  28449  ftc1anclem7  28478  ftc1anc  28480  modfsummodslem1  30245  fsumsplitsnun  30247  sucidVD  31613  bnj553  31896  bnj966  31942  bnj1442  32045  hdmaplem2N  35422  hdmaplem3  35423
  Copyright terms: Public domain W3C validator