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

Theorem elun2 3613
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 3609 . 2  |-  B  C_  ( C  u.  B
)
21sseli 3440 1  |-  ( A  e.  B  ->  A  e.  ( C  u.  B
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1844    u. cun 3414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-v 3063  df-un 3421  df-in 3423  df-ss 3430
This theorem is referenced by:  dftpos4  6979  wfrlem14  7036  tfrlem11  7093  findcard2d  7798  cantnfp1lem1  8131  cantnfp1lem3  8133  cantnfp1lem1OLD  8157  cantnfp1lem3OLD  8159  tc2  8207  rankunb  8302  rankelun  8324  dfac2  8545  cfsmolem  8684  isfin4-3  8729  zornn0g  8919  mnfxr  11378  supxrun  11562  fsumsplitsnun  13723  sumsplit  13736  modfsummodslem1  13759  prmreclem5  14649  acsfiindd  16133  lspsolv  18111  mplcoe1  18449  maducoeval2  19436  restntr  19978  1stckgenlem  20348  fbun  20635  filuni  20680  ufileu  20714  alexsubALTlem4  20844  tmdgsum  20888  icccmplem2  21622  aannenlem2  23019  aalioulem2  23023  ebtwntg  24714  elntg  24716  bnj553  29296  bnj966  29342  bnj1442  29445  mrsubrn  29738  elmrsubrn  29745  mvhf  29783  msubvrs  29785  altxpsspw  30328  mbfresfi  31446  itg2addnclem2  31453  ftc1anclem7  31482  ftc1anc  31484  hdmaplem2N  34805  hdmaplem3  34806  sucidVD  36716  mccllem  36986  limcresiooub  37029  limcresioolb  37030  dvmptfprodlem  37122  dvmptfprod  37123  dvnprodlem1  37124  dvnprodlem2  37125  fourierdlem20  37290  fourierdlem38  37308  fourierdlem48  37318  fourierdlem49  37319  fourierdlem51  37321  fourierdlem62  37332  fourierdlem63  37333  fourierdlem64  37334  fourierdlem65  37335  fourierdlem71  37341  fouriersw  37395
  Copyright terms: Public domain W3C validator