Theorem unex 6598

Description: The union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 1-Jul-1994.)

Hypotheses

Ref	Expression
unex.1
unex.2

Assertion

Ref	Expression
unex

Proof of Theorem unex

Step	Hyp	Ref	Expression
1		unex.1	. . 3
2		unex.2	. . 3
3	1, 2	unipr 4262	. 2
4		prex 4694	. . 3
5	4	uniex 6596	. 2
6	3, 5	eqeltrri 2542	1

Syntax hints:  e.wcel 1818  cvv 3109  u.cun 3473  {cpr 4031  U.cuni 4249

This theorem is referenced by:  tpex  6599  unexb  6600  fvclex  6772  ralxpmap  7488  unen  7618  enfixsn  7646  sbthlem10  7656  unxpdomlem3  7746  isinf  7753  findcard2  7780  ac6sfi  7784  pwfilem  7834  fiin  7902  cnfcomlem  8164  cnfcomlemOLD  8172  trcl  8180  tc2  8194  rankxpu  8315  rankxplim  8318  rankxplim3  8320  r0weon  8411  infxpenlem  8412  dfac4  8524  dfac2  8532  kmlem2  8552  cdafn  8570  cfsmolem  8671  isfin1-3  8787  axdc2lem  8849  axdc3lem4  8854  axcclem  8858  ttukeylem3  8912  gchac  9080  wunex2  9137  wuncval2  9146  inar1  9174  nn0ex  10826  xrex  11246  hashbclem  12501  ccatfn  12591  incexclem  13648  ramub1lem2  14545  prdsval  14852  imasval  14908  ipoval  15784  fpwipodrs  15794  plusffval  15877  staffval  17496  scaffval  17530  lpival  17893  psrval  18011  xrsex  18433  ipffval  18683  islindf4  18873  neitr  19681  leordtval2  19713  comppfsc  20033  1stckgen  20055  dfac14  20119  ptcmpfi  20314  hausflim  20482  flimclslem  20485  alexsubALTlem2  20548  nmfval  21109  icccmplem2  21328  tchex  21660  tchnmfval  21671  taylfval  22754  legval  23971  axlowdimlem15  24259  axlowdim  24264  eengv  24282  constr3lem1  24645  constr3cyclpe  24663  3v3e3cycl2  24664  ordtconlem1  27906  sxbrsigalem2  28257  subfacp1lem3  28626  subfacp1lem5  28628  erdszelem8  28642  mrexval  28861  mrsubcv  28870  mrsubff  28872  mrsubccat  28878  elmrsubrn  28880  finixpnum  30038  rrnval  30323  elrfi  30626  istopclsd  30632  mzpcompact2lem  30684  eldioph2lem1  30693  eldioph2lem2  30694  eldioph4b  30745  diophren  30747  ttac  30978  pwslnmlem2  31039  dfacbasgrp  31057  mendval  31132  idomsubgmo  31155  fnchoice  31404  limcresiooub  31648  limcresioolb  31649  fourierdlem48  31937  fourierdlem49  31938  fourierdlem102  31991  fourierdlem114  32003  bnj918  33824  lsatset  34715  ldualset  34850  pclfinN  35624  dvaset  36731  dvhset  36808  hlhilset  37664  superuncl  37753  ssuncl  37755  sssymdifcl  37757  trclubg  37785

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-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691  ax-un 6592

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-ne 2654  df-rex 2813  df-v 3111  df-dif 3478  df-un 3480  df-nul 3785  df-sn 4030  df-pr 4032  df-uni 4250