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 3451   ∪ cun 3897

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 2733  ax-sep 5249  ax-pr 5391  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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916  df-sn 4585  df-pr 4587  df-uni 4868

This theorem is used by:  tpex  7751  fvclex  7960  naddcllem  8669  ralxpmap  8908  unen  9057  undom  9068  enfixsn  9089  sbthlem10  9099  dif1en  9161  findcard2  9164  unxpdomlem3  9233  isinf  9240  ac6sfi  9259  pwfilem  9293  cnfcomlem  9684  trcl  9713  tc2  9725  rankxpu  9874  rankxplim  9877  rankxplim3  9879  r0weon  10072  infxpenlem  10073  dfac4  10182  dfac2b  10190  kmlem2  10211  cfsmolem  10329  isfin1-3  10445  axdc2lem  10507  axdc3lem4  10512  axcclem  10516  ttukeylem3  10570  gchac  10747  wunex2  10804  wuncval2  10813  inar1  10841  nn0ex  12593  xrex  13096  seqexw  14140  hashbclem  14577  incexclem  15985  ramub1lem2  17185  prdsval  17606  imasval  17663  ipoval  18684  plusffval  18802  smndex1bas  19085  smndex1sgrp  19087  smndex1mnd  19089  smndex1id  19090  grpinvfval  19169  grpsubfval  19174  mulgfval  19259  staffval  21078  scaffval  21135  lpival  21628  cnfldex  21661  xrsex  21675  ipffval  21934  islindf4  22124  psrval  22203  neitr  23478  leordtval2  23510  comppfsc  23831  1stckgen  23853  dfac14  23917  ptcmpfi  24112  hausflim  24280  flimclslem  24283  alexsubALTlem2  24347  nmfval  24887  icccmplem2  25123  tcphex  25518  tchnmfval  25529  taylfval  26668  lrrecse  28310  addsval  28330  negsval  28393  negsid  28409  mulsval  28477  mulsproplem9  28492  precsexlem4  28578  precsexlem5  28579  oncutlt  28632  onaddscl  28645  legval  29029  axlowdimlem15  29516  axlowdim  29521  eengv  29539  uhgrunop  29635  upgrunop  29679  umgrunop  29681  padct  33292  cycpmconjslem2  33698  rlocbas  33811  rlocaddval  33812  rlocmulval  33813  idlsrgval  34017  ordtconnlem1  34538  sxbrsigalem2  34901  actfunsnf1o  35216  actfunsnrndisj  35217  reprsuc  35227  breprexplema  35242  bnj918  35380  fineqvac  35757  subfacp1lem3  35916  subfacp1lem5  35918  erdszelem8  35932  satfvsuclem1  36093  satf0suc  36110  fmlasuc0  36118  mrexval  36235  mrsubcv  36244  mrsubff  36246  mrsubccat  36252  elmrsubrn  36254  dfttc4lem2  37287  rdgssun  38269  exrecfnlem  38270  finixpnum  38496  poimirlem4  38510  poimirlem15  38521  poimirlem28  38534  dfproplem  38609  rrnval  38729  lsatset  40015  ldualset  40150  pclfinN  40925  dvaset  42030  dvhset  42106  hlhilset  42959  evlselv  43579  elrfi  43658  istopclsd  43664  mzpcompact2lem  43715  eldioph2lem1  43724  eldioph2lem2  43725  eldioph4b  43771  diophren  43773  ttac  43996  pwslnmlem2  44053  dfacbasgrp  44068  mendval  44139  idomsubgmo  44153  superuncl  44527  ssuncl  44529  sssymdifcl  44531  rclexi  44574  trclexi  44579  rtrclexi  44580  dfrtrcl5  44588  dfrcl2  44633  comptiunov2i  44665  cotrclrcl  44701  frege83  44905  frege110  44932  frege133  44955  clsk1indlem3  45002  permaxinf2lem  45954  fnchoice  45989  limcresiooub  46596  limcresioolb  46597  fourierdlem48  47108  fourierdlem49  47109  fourierdlem102  47162  fourierdlem114  47174  sge0resplit  47360  elpglem2  50749