Theorem unexg 7676

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

Assertion

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

Proof of Theorem unexg

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  Vcvv 3436   ∪ cun 3900  {cpr 4578  ∪ cuni 4859

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 2113  ax-9 2121  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370  ax-un 7668

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-sn 4577  df-pr 4579  df-uni 4860

This theorem is referenced by:  unex  7677  unexb  7680  xpexg  7683  unexd  7687  difex2  7693  difsnexi  7694  eldifpw  7701  pwuncl  7703  ordunpr  7756  soex  7851  fnse  8063  suppun  8114  tposexg  8170  frrlem13  8228  tfrlem12  8308  tfrlem16  8312  elmapresaun  8804  ralxpmap  8820  undifixp  8858  undom  8978  domunsncan  8990  domssex2  9050  domssex  9051  mapunen  9059  sbthfilem  9107  fsuppunbi  9273  elfiun  9314  brwdom2  9459  unwdomg  9470  djuex  9798  djuexALT  9812  alephprc  9987  djudoml  10073  infunabs  10094  fin23lem11  10205  axdc2lem  10336  ttukeylem1  10397  fpwwe2lem12  10530  wunex2  10626  wuncval2  10635  hashunx  14290  hashf1lem1  14359  trclexlem  14898  trclun  14918  relexp0g  14926  relexpsucnnr  14929  isstruct2  17057  setsvalg  17074  setsid  17115  yonffth  18187  pwmndgplus  18840  dmdprdsplit2  19958  basdif0  22866  fiuncmp  23317  refun0  23428  ptbasfi  23494  dfac14lem  23530  ptrescn  23552  xkoptsub  23567  filconn  23796  isufil2  23821  ufileu  23832  filufint  23833  fmfnfmlem4  23870  fmfnfm  23871  fclsfnflim  23940  flimfnfcls  23941  ptcmplem1  23965  elply2  26126  plyss  26129  noeta2  27722  etasslt2  27753  scutbdaybnd2lim  27756  wlkp1lem4  29651  resf1o  32708  tocycfv  33073  tocycf  33081  locfinref  33849  esumsplit  34061  esumpad2  34064  sseqval  34396  bnj1149  34799  tz9.1regs  35118  satfvsuc  35393  satf0suclem  35407  sat1el2xp  35411  fmlasuc0  35416  altxpexg  36011  hfun  36211  refssfne  36391  topjoin  36398  weiunse  36501  bj-2uplex  37055  ptrest  37658  poimirlem3  37662  paddval  39836  evlselvlem  42618  elrfi  42726  rtrclexlem  43648  clcnvlem  43655  cnvrcl0  43657  dfrtrcl5  43661  iunrelexp0  43734  relexpxpmin  43749  brtrclfv2  43759  sge0resplit  46443  sge0split  46446  setsv  47408  setrec1lem4  49721