Theorem unexg 7683

Description: The union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 18-Sep-2006.) Prove unexg 7683 first and then unex 7684 and unexb 7687 from it. (Revised by BJ, 21-Jul-2025.)

Assertion

Ref	Expression
unexg	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)

Proof of Theorem unexg

Step	Hyp	Ref	Expression
1		uniprg 4877	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵))
2		prex 5379	. . . 4 ⊢ {𝐴, 𝐵} ∈ V
3	2	a1i 11	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)
4	3	uniexd 7682	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ {𝐴, 𝐵} ∈ V)
5	1, 4	eqeltrrd 2829	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Vcvv 3438   ∪ cun 3903  {cpr 4581  ∪ cuni 4861

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7675

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-sn 4580  df-pr 4582  df-uni 4862

This theorem is referenced by:  unex  7684  unexb  7687  xpexg  7690  unexd  7694  difex2  7700  difsnexi  7701  eldifpw  7708  pwuncl  7710  ordunpr  7765  soex  7861  fnse  8073  suppun  8124  tposexg  8180  frrlem13  8238  tfrlem12  8318  tfrlem16  8322  elmapresaun  8814  ralxpmap  8830  undifixp  8868  undom  8989  domunsncan  9001  domssex2  9061  domssex  9062  mapunen  9070  sbthfilem  9122  fsuppunbi  9298  elfiun  9339  brwdom2  9484  unwdomg  9495  djuex  9823  djuexALT  9837  alephprc  10012  djudoml  10098  infunabs  10119  fin23lem11  10230  axdc2lem  10361  ttukeylem1  10422  fpwwe2lem12  10555  wunex2  10651  wuncval2  10660  hashunx  14311  hashf1lem1  14380  trclexlem  14919  trclun  14939  relexp0g  14947  relexpsucnnr  14950  isstruct2  17078  setsvalg  17095  setsid  17136  yonffth  18208  pwmndgplus  18827  dmdprdsplit2  19945  basdif0  22856  fiuncmp  23307  refun0  23418  ptbasfi  23484  dfac14lem  23520  ptrescn  23542  xkoptsub  23557  filconn  23786  isufil2  23811  ufileu  23822  filufint  23823  fmfnfmlem4  23860  fmfnfm  23861  fclsfnflim  23930  flimfnfcls  23931  ptcmplem1  23955  elply2  26117  plyss  26120  noeta2  27713  etasslt2  27743  scutbdaybnd2lim  27746  wlkp1lem4  29638  resf1o  32686  tocycfv  33064  tocycf  33072  locfinref  33807  esumsplit  34019  esumpad2  34022  sseqval  34355  bnj1149  34758  tz9.1regs  35066  satfvsuc  35333  satf0suclem  35347  sat1el2xp  35351  fmlasuc0  35356  altxpexg  35951  hfun  36151  refssfne  36331  topjoin  36338  weiunse  36441  bj-2uplex  36995  ptrest  37598  poimirlem3  37602  paddval  39777  evlselvlem  42559  elrfi  42667  rtrclexlem  43589  clcnvlem  43596  cnvrcl0  43598  dfrtrcl5  43602  iunrelexp0  43675  relexpxpmin  43690  brtrclfv2  43700  sge0resplit  46388  sge0split  46391  setsv  47363  setrec1lem4  49676