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

Theorem elun2 3671
Description: Membership law for union of classes. (Contributed by NM, 30-Aug-1993.)
Assertion
Ref Expression
elun2

Proof of Theorem elun2
StepHypRef Expression
1 ssun2 3667 . 2
21sseli 3499 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818  u.cun 3473
This theorem is referenced by:  dftpos4  6993  tfrlem11  7076  findcard2d  7782  cantnfp1lem1  8118  cantnfp1lem3  8120  cantnfp1lem1OLD  8144  cantnfp1lem3OLD  8146  tc2  8194  rankunb  8289  rankelun  8311  dfac2  8532  cfsmolem  8671  isfin4-3  8716  zornn0g  8906  mnfxr  11352  supxrun  11536  fsumsplitsnun  13570  sumsplit  13583  modfsummodslem1  13606  prmreclem5  14438  acsfiindd  15807  lspsolv  17789  mplcoe1  18127  maducoeval2  19142  restntr  19683  1stckgenlem  20054  fbun  20341  filuni  20386  ufileu  20420  alexsubALTlem4  20550  tmdgsum  20594  icccmplem2  21328  aannenlem2  22725  aalioulem2  22729  ebtwntg  24285  elntg  24287  mrsubrn  28873  elmrsubrn  28880  mvhf  28918  msubvrs  28920  wfrlem14  29356  altxpsspw  29627  mbfresfi  30061  itg2addnclem2  30067  ftc1anclem7  30096  ftc1anc  30098  mccllem  31605  limcresiooub  31648  limcresioolb  31649  dvmptfprodlem  31741  dvmptfprod  31742  dvnprodlem1  31743  dvnprodlem2  31744  fourierdlem20  31909  fourierdlem38  31927  fourierdlem48  31937  fourierdlem49  31938  fourierdlem51  31940  fourierdlem62  31951  fourierdlem63  31952  fourierdlem64  31953  fourierdlem65  31954  fourierdlem71  31960  fouriersw  32014  sucidVD  33672  bnj553  33956  bnj966  34002  bnj1442  34105  hdmaplem2N  37499  hdmaplem3  37500
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator