Theorem unex 7761

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	. 2 ⊢ 𝐴 ∈ V
2		unex.2	. 2 ⊢ 𝐵 ∈ V
3		unexg 7760	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ∪ 𝐵) ∈ V)
4	1, 2, 3	mp2an 705	1 ⊢ (𝐴 ∪ 𝐵) ∈ V

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450   ∪ cun 4149

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-un 4151  df-sn 4585  df-pr 4587  df-uni 4867

This theorem is used by:  tpex  7762  fvclex  7971  naddcllem  8688  ralxpmap  8927  unen  9076  undom  9087  enfixsn  9108  sbthlem10  9118  dif1en  9180  findcard2  9183  unxpdomlem3  9252  isinf  9259  ac6sfi  9278  pwfilem  9312  cnfcomlem  9703  trcl  9732  tc2  9744  rankxpu  9896  rankxplim  9899  rankxplim3  9901  r0weon  10094  infxpenlem  10095  dfac4  10204  dfac2b  10212  kmlem2  10233  cfsmolem  10351  isfin1-3  10467  axdc2lem  10529  axdc3lem4  10534  axcclem  10538  ttukeylem3  10592  gchac  10769  wunex2  10826  wuncval2  10835  inar1  10863  nn0ex  12615  xrex  13118  seqexw  14163  hashbclem  14600  incexclem  16010  ramub1lem2  17210  prdsval  17631  imasval  17688  ipoval  18709  plusffval  18827  smndex1bas  19110  smndex1sgrp  19112  smndex1mnd  19114  smndex1id  19115  grpinvfval  19194  grpsubfval  19199  mulgfval  19284  staffval  21103  scaffval  21160  lpival  21653  cnfldex  21686  xrsex  21700  ipffval  21959  islindf4  22149  psrval  22228  neitr  23503  leordtval2  23535  comppfsc  23856  1stckgen  23878  dfac14  23942  ptcmpfi  24137  hausflim  24305  flimclslem  24308  alexsubALTlem2  24372  nmfval  24912  icccmplem2  25148  tcphex  25543  tchnmfval  25554  taylfval  26691  lrrecse  28333  addsval  28353  negsval  28416  negsid  28432  mulsval  28500  mulsproplem9  28515  precsexlem4  28601  precsexlem5  28602  oncutlt  28655  onaddscl  28668  legval  29052  axlowdimlem15  29539  axlowdim  29544  eengv  29562  uhgrunop  29658  upgrunop  29702  umgrunop  29704  padct  33357  cycpmconjslem2  33762  rlocbas  33875  rlocaddval  33876  rlocmulval  33877  idlsrgval  34081  ordtconnlem1  34602  sxbrsigalem2  34964  actfunsnf1o  35279  actfunsnrndisj  35280  reprsuc  35290  breprexplema  35305  bnj918  35443  fineqvac  35840  subfacp1lem3  36033  subfacp1lem5  36035  erdszelem8  36049  satfvsuclem1  36210  satf0suc  36227  fmlasuc0  36235  mrexval  36352  mrsubcv  36361  mrsubff  36363  mrsubccat  36369  elmrsubrn  36371  dfttc4lem2  37409  rdgssun  38394  exrecfnlem  38395  finixpnum  38621  poimirlem4  38635  poimirlem15  38646  poimirlem28  38659  dfproplem  38734  rrnval  38854  lsatset  40140  ldualset  40275  pclfinN  41050  dvaset  42155  dvhset  42231  hlhilset  43084  evlselv  43710  elrfi  43798  istopclsd  43804  mzpcompact2lem  43855  eldioph2lem1  43864  eldioph2lem2  43865  eldioph4b  43911  diophren  43913  ttac  44136  pwslnmlem2  44188  dfacbasgrp  44203  mendval  44274  idomsubgmo  44288  superuncl  44662  ssuncl  44664  sssymdifcl  44666  rclexi  44708  trclexi  44713  rtrclexi  44714  dfrtrcl5  44722  dfrcl2  44767  comptiunov2i  44799  cotrclrcl  44835  frege83  45039  frege110  45066  frege133  45089  clsk1indlem3  45136  permaxinf2lem  46095  fnchoice  46139  limcresiooub  46745  limcresioolb  46746  fourierdlem48  47257  fourierdlem49  47258  fourierdlem102  47311  fourierdlem114  47323  sge0resplit  47509  parcatid2  50856  parcatid  50857  parmapfunc2  50867  elpglem2  50973