Theorem unex 7750

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3453   ∪ cun 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pr 5402  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-ss 3919  df-sn 4588  df-pr 4590  df-uni 4871

This theorem is used by:  tpex  7751  fvclex  7960  naddcllem  8668  ralxpmap  8907  unen  9056  undom  9067  enfixsn  9088  sbthlem10  9098  dif1en  9160  findcard2  9163  unxpdomlem3  9232  isinf  9239  ac6sfi  9258  pwfilem  9291  cnfcomlem  9682  trcl  9711  tc2  9723  rankxpu  9862  rankxplim  9865  rankxplim3  9867  r0weon  10019  infxpenlem  10020  dfac4  10129  dfac2b  10137  kmlem2  10158  cfsmolem  10276  isfin1-3  10392  axdc2lem  10454  axdc3lem4  10459  axcclem  10463  ttukeylem3  10517  gchac  10694  wunex2  10751  wuncval2  10760  inar1  10788  nn0ex  12538  xrex  13041  seqexw  14085  hashbclem  14521  incexclem  15929  ramub1lem2  17125  prdsval  17546  imasval  17603  ipoval  18624  plusffval  18742  smndex1bas  19024  smndex1sgrp  19026  smndex1mnd  19028  smndex1id  19029  grpinvfval  19108  grpsubfval  19113  mulgfval  19198  staffval  21013  scaffval  21070  lpival  21561  cnfldex  21594  xrsex  21608  ipffval  21867  islindf4  22057  psrval  22136  neitr  23411  leordtval2  23443  comppfsc  23764  1stckgen  23786  dfac14  23850  ptcmpfi  24045  hausflim  24213  flimclslem  24216  alexsubALTlem2  24280  nmfval  24820  icccmplem2  25056  tcphex  25451  tchnmfval  25462  taylfval  26602  lrrecse  28215  addsval  28235  negsval  28298  negsid  28314  mulsval  28382  mulsproplem9  28397  precsexlem4  28483  precsexlem5  28484  oncutlt  28537  onaddscl  28550  legval  28934  axlowdimlem15  29421  axlowdim  29426  eengv  29444  uhgrunop  29540  upgrunop  29584  umgrunop  29586  padct  33197  cycpmconjslem2  33603  rlocbas  33716  rlocaddval  33717  rlocmulval  33718  idlsrgval  33921  ordtconnlem1  34442  sxbrsigalem2  34805  actfunsnf1o  35120  actfunsnrndisj  35121  reprsuc  35131  breprexplema  35146  bnj918  35284  fineqvac  35650  subfacp1lem3  35769  subfacp1lem5  35771  erdszelem8  35785  satfvsuclem1  35946  satf0suc  35963  fmlasuc0  35971  mrexval  36088  mrsubcv  36097  mrsubff  36099  mrsubccat  36105  elmrsubrn  36107  dfttc4lem2  37156  rdgssun  38140  exrecfnlem  38141  finixpnum  38367  poimirlem4  38381  poimirlem15  38392  poimirlem28  38405  rrnval  38585  lsatset  39871  ldualset  40006  pclfinN  40781  dvaset  41886  dvhset  41962  hlhilset  42815  evlselv  43443  elrfi  43547  istopclsd  43553  mzpcompact2lem  43604  eldioph2lem1  43613  eldioph2lem2  43614  eldioph4b  43660  diophren  43662  ttac  43885  pwslnmlem2  43942  dfacbasgrp  43957  mendval  44028  idomsubgmo  44042  superuncl  44416  ssuncl  44418  sssymdifcl  44420  rclexi  44463  trclexi  44468  rtrclexi  44469  dfrtrcl5  44477  dfrcl2  44522  comptiunov2i  44554  cotrclrcl  44590  frege83  44794  frege110  44821  frege133  44844  clsk1indlem3  44891  permaxinf2lem  45843  fnchoice  45871  limcresiooub  46478  limcresioolb  46479  fourierdlem48  46990  fourierdlem49  46991  fourierdlem102  47044  fourierdlem114  47056  sge0resplit  47242  elpglem2  50646