Theorem elun1 3670

Description: Membership law for union of classes. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
elun1

Proof of Theorem elun1

Step	Hyp	Ref	Expression
1		ssun1 3666	. 2
2	1	sseli 3499	1

Syntax hints:  ->wi 4  e.wcel 1818  u.cun 3473

This theorem is referenced by:  brtpos  6983  dftpos4  6993  domunsncan  7637  unxpdomlem2  7745  rankunb  8289  rankelun  8311  fin1a2lem10  8810  zornn0g  8906  xrsupexmnf  11525  xrinfmexpnf  11526  sumsplit  13583  prmreclem5  14438  lbsextlem3  17806  restntr  19683  comppfsc  20033  1stckgenlem  20054  fbun  20341  filcon  20384  filuni  20386  alexsubALTlem4  20550  ovolfiniun  21912  volfiniun  21957  elplyd  22599  ply1term  22601  aannenlem2  22725  aalioulem2  22729  eengbas  24284  ecgrtg  24286  vdgrf  24898  gsumle  27770  mrsubcn  28879  mrsubco  28881  altxpsspw  29627  mbfresfi  30061  itg2addnclem2  30067  ftc1anclem7  30096  ftc1anc  30098  mccllem  31605  limcresiooub  31648  limcresioolb  31649  dvmptfprodlem  31741  dvnprodlem2  31744  fourierdlem48  31937  fourierdlem49  31938  fourierdlem51  31940  fourierdlem54  31943  fourierdlem62  31951  fourierdlem71  31960  fourierdlem103  31992  fourierdlem104  31993  fourierdlem114  32003  fouriersw  32014  sucidALTVD  33670  sucidALT  33671  bnj1498  34117  hdmaplem1  37498  hdmap1eulem  37551

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