Theorem unexg 7682

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

Assertion

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

Proof of Theorem unexg

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  Vcvv 3437   ∪ cun 3896  {cpr 4577  ∪ cuni 4858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372  ax-un 7674

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-sn 4576  df-pr 4578  df-uni 4859

This theorem is referenced by:  unex  7683  unexb  7686  xpexg  7689  unexd  7693  difex2  7699  difsnexi  7700  eldifpw  7707  pwuncl  7709  ordunpr  7762  soex  7857  fnse  8069  suppun  8120  tposexg  8176  frrlem13  8234  tfrlem12  8314  tfrlem16  8318  elmapresaun  8810  ralxpmap  8826  undifixp  8864  undom  8985  domunsncan  8997  domssex2  9057  domssex  9058  mapunen  9066  sbthfilem  9114  fsuppunbi  9280  elfiun  9321  brwdom2  9466  unwdomg  9477  djuex  9808  djuexALT  9822  alephprc  9997  djudoml  10083  infunabs  10104  fin23lem11  10215  axdc2lem  10346  ttukeylem1  10407  fpwwe2lem12  10540  wunex2  10636  wuncval2  10645  hashunx  14295  hashf1lem1  14364  trclexlem  14903  trclun  14923  relexp0g  14931  relexpsucnnr  14934  isstruct2  17062  setsvalg  17079  setsid  17120  yonffth  18192  pwmndgplus  18845  dmdprdsplit2  19962  basdif0  22869  fiuncmp  23320  refun0  23431  ptbasfi  23497  dfac14lem  23533  ptrescn  23555  xkoptsub  23570  filconn  23799  isufil2  23824  ufileu  23835  filufint  23836  fmfnfmlem4  23873  fmfnfm  23874  fclsfnflim  23943  flimfnfcls  23944  ptcmplem1  23968  elply2  26129  plyss  26132  noeta2  27725  etasslt2  27756  scutbdaybnd2lim  27759  wlkp1lem4  29655  resf1o  32717  tocycfv  33085  tocycf  33093  locfinref  33875  esumsplit  34087  esumpad2  34090  sseqval  34422  bnj1149  34825  tz9.1regs  35151  satfvsuc  35426  satf0suclem  35440  sat1el2xp  35444  fmlasuc0  35449  altxpexg  36043  hfun  36243  refssfne  36423  topjoin  36430  weiunse  36533  bj-2uplex  37087  ptrest  37679  poimirlem3  37683  paddval  39917  evlselvlem  42704  elrfi  42811  rtrclexlem  43733  clcnvlem  43740  cnvrcl0  43742  dfrtrcl5  43746  iunrelexp0  43819  relexpxpmin  43834  brtrclfv2  43844  sge0resplit  46528  sge0split  46531  setsv  47502  setrec1lem4  49815