Theorem unexg 7697

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

Assertion

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

Proof of Theorem unexg

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  Vcvv 3429   ∪ cun 3887  {cpr 4569  ∪ cuni 4850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906  df-sn 4568  df-pr 4570  df-uni 4851

This theorem is referenced by:  unex  7698  unexb  7701  xpexg  7704  unexd  7708  difex2  7714  difsnexi  7715  eldifpw  7722  pwuncl  7724  ordunpr  7777  soex  7872  fnse  8083  suppun  8134  tposexg  8190  frrlem13  8248  tfrlem12  8328  tfrlem16  8332  elmapresaun  8828  ralxpmap  8844  undifixp  8882  undom  9003  domunsncan  9015  domssex2  9075  domssex  9076  mapunen  9084  sbthfilem  9132  fsuppunbi  9302  elfiun  9343  brwdom2  9488  unwdomg  9499  djuex  9832  djuexALT  9846  alephprc  10021  djudoml  10107  infunabs  10128  fin23lem11  10239  axdc2lem  10370  ttukeylem1  10431  fpwwe2lem12  10565  wunex2  10661  wuncval2  10670  hashunx  14348  hashf1lem1  14417  trclexlem  14956  trclun  14976  relexp0g  14984  relexpsucnnr  14987  isstruct2  17119  setsvalg  17136  setsid  17177  yonffth  18250  pwmndgplus  18906  dmdprdsplit2  20023  basdif0  22918  fiuncmp  23369  refun0  23480  ptbasfi  23546  dfac14lem  23582  ptrescn  23604  xkoptsub  23619  filconn  23848  isufil2  23873  ufileu  23884  filufint  23885  fmfnfmlem4  23922  fmfnfm  23923  fclsfnflim  23992  flimfnfcls  23993  ptcmplem1  24017  elply2  26161  plyss  26164  noeta2  27753  etaslts2  27786  cutbdaybnd2lim  27789  wlkp1lem4  29743  resf1o  32803  tocycfv  33170  tocycf  33178  locfinref  33985  esumsplit  34197  esumpad2  34200  sseqval  34532  bnj1149  34934  tz9.1regs  35278  satfvsuc  35543  satf0suclem  35557  sat1el2xp  35561  fmlasuc0  35566  altxpexg  36160  hfun  36360  refssfne  36540  topjoin  36547  weiunse  36650  ttcsnexg  36702  bj-2uplex  37329  ptrest  37940  poimirlem3  37944  paddval  40244  evlselvlem  43019  elrfi  43126  rtrclexlem  44043  clcnvlem  44050  cnvrcl0  44052  dfrtrcl5  44056  iunrelexp0  44129  relexpxpmin  44144  brtrclfv2  44154  sge0resplit  46834  sge0split  46837  setsv  47838  setrec1lem4  50165