Theorem unex 7195

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	⊢ 𝐴 ∈ V
unex.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
unex	⊢ (𝐴 ∪ 𝐵) ∈ V

Proof of Theorem unex

Step	Hyp	Ref	Expression
1		unex.1	. . 3 ⊢ 𝐴 ∈ V
2		unex.2	. . 3 ⊢ 𝐵 ∈ V
3	1, 2	unipr 4654	. 2 ⊢ ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵)
4		prex 5112	. . 3 ⊢ {𝐴, 𝐵} ∈ V
5	4	uniex 7192	. 2 ⊢ ∪ {𝐴, 𝐵} ∈ V
6	3, 5	eqeltrri 2893	1 ⊢ (𝐴 ∪ 𝐵) ∈ V

Syntax hints:   ∈ wcel 2157  Vcvv 3402   ∪ cun 3778  {cpr 4383  ∪ cuni 4641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988  ax-nul 4996  ax-pr 5109  ax-un 7188

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-rex 3113  df-v 3404  df-dif 3783  df-un 3785  df-nul 4128  df-sn 4382  df-pr 4384  df-uni 4642

This theorem is referenced by:  tpex  7196  unexb  7197  fvclex  7377  ralxpmap  8153  unen  8288  enfixsn  8317  sbthlem10  8327  unxpdomlem3  8414  isinf  8421  findcard2  8448  ac6sfi  8452  pwfilem  8508  fiin  8576  cnfcomlem  8852  trcl  8860  tc2  8874  rankxpu  8995  rankxplim  8998  rankxplim3  9000  r0weon  9127  infxpenlem  9128  dfac4  9237  dfac2b  9245  dfac2OLD  9247  kmlem2  9267  cdafn  9285  cfsmolem  9386  isfin1-3  9502  axdc2lem  9564  axdc3lem4  9569  axcclem  9573  ttukeylem3  9627  gchac  9797  wunex2  9854  wuncval2  9863  inar1  9891  nn0ex  11584  xrex  12062  hashbclem  13472  incexclem  14809  ramub1lem2  15967  prdsval  16339  imasval  16395  ipoval  17378  fpwipodrs  17388  plusffval  17471  staffval  19070  scaffval  19104  lpival  19473  psrval  19590  xrsex  19988  ipffval  20222  islindf4  20407  neitr  21218  leordtval2  21250  comppfsc  21569  1stckgen  21591  dfac14  21655  ptcmpfi  21850  hausflim  22018  flimclslem  22021  alexsubALTlem2  22085  nmfval  22626  icccmplem2  22859  tchex  23248  tchnmfval  23259  taylfval  24349  legval  25715  axlowdimlem15  26072  axlowdim  26077  eengv  26095  uhgrunop  26206  upgrunop  26250  umgrunop  26252  padct  29846  ordtconnlem1  30317  sxbrsigalem2  30695  actfunsnf1o  31029  actfunsnrndisj  31030  reprsuc  31040  breprexplema  31055  bnj918  31180  subfacp1lem3  31508  subfacp1lem5  31510  erdszelem8  31524  mrexval  31742  mrsubcv  31751  mrsubff  31753  mrsubccat  31759  elmrsubrn  31761  cnfinltrel  33575  finixpnum  33725  poimirlem4  33744  poimirlem15  33755  poimirlem28  33768  rrnval  33955  lsatset  34788  ldualset  34923  pclfinN  35698  dvaset  36803  dvhset  36879  hlhilset  37732  elrfi  37776  istopclsd  37782  mzpcompact2lem  37833  eldioph2lem1  37842  eldioph2lem2  37843  eldioph4b  37894  diophren  37896  ttac  38121  pwslnmlem2  38181  dfacbasgrp  38196  mendval  38271  idomsubgmo  38294  superuncl  38390  ssuncl  38392  sssymdifcl  38394  rclexi  38439  trclexi  38444  rtrclexi  38445  dfrtrcl5  38453  dfrcl2  38483  comptiunov2i  38515  cotrclrcl  38551  frege83  38757  frege110  38784  frege133  38807  clsk1indlem3  38858  isotone1  38863  fnchoice  39699  limcresiooub  40371  limcresioolb  40372  fourierdlem48  40867  fourierdlem49  40868  fourierdlem102  40921  fourierdlem114  40933  sge0resplit  41119  elpglem2  43043