Theorem unexg 7722

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

Assertion

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

Proof of Theorem unexg

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Vcvv 3450   ∪ cun 3915  {cpr 4594  ∪ cuni 4874

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

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 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-sn 4593  df-pr 4595  df-uni 4875

This theorem is referenced by:  unex  7723  unexb  7726  xpexg  7729  unexd  7733  difex2  7739  difsnexi  7740  eldifpw  7747  pwuncl  7749  ordunpr  7804  soex  7900  fnse  8115  suppun  8166  tposexg  8222  frrlem13  8280  tfrlem12  8360  tfrlem16  8364  elmapresaun  8856  ralxpmap  8872  undifixp  8910  undom  9033  undomOLD  9034  domunsncan  9046  domssex2  9107  domssex  9108  mapunen  9116  sbthfilem  9168  fsuppunbi  9347  elfiun  9388  brwdom2  9533  unwdomg  9544  djuex  9868  djuexALT  9882  alephprc  10059  djudoml  10145  infunabs  10166  fin23lem11  10277  axdc2lem  10408  ttukeylem1  10469  fpwwe2lem12  10602  wunex2  10698  wuncval2  10707  hashunx  14358  hashf1lem1  14427  trclexlem  14967  trclun  14987  relexp0g  14995  relexpsucnnr  14998  isstruct2  17126  setsvalg  17143  setsid  17184  yonffth  18252  pwmndgplus  18869  dmdprdsplit2  19985  basdif0  22847  fiuncmp  23298  refun0  23409  ptbasfi  23475  dfac14lem  23511  ptrescn  23533  xkoptsub  23548  filconn  23777  isufil2  23802  ufileu  23813  filufint  23814  fmfnfmlem4  23851  fmfnfm  23852  fclsfnflim  23921  flimfnfcls  23922  ptcmplem1  23946  elply2  26108  plyss  26111  noeta2  27703  etasslt2  27733  scutbdaybnd2lim  27736  wlkp1lem4  29611  resf1o  32660  tocycfv  33073  tocycf  33081  locfinref  33838  esumsplit  34050  esumpad2  34053  sseqval  34386  bnj1149  34789  satfvsuc  35355  satf0suclem  35369  sat1el2xp  35373  fmlasuc0  35378  altxpexg  35973  hfun  36173  refssfne  36353  topjoin  36360  weiunse  36463  bj-2uplex  37017  ptrest  37620  poimirlem3  37624  paddval  39799  evlselvlem  42581  elrfi  42689  rtrclexlem  43612  clcnvlem  43619  cnvrcl0  43621  dfrtrcl5  43625  iunrelexp0  43698  relexpxpmin  43713  brtrclfv2  43723  sge0resplit  46411  sge0split  46414  setsv  47383  setrec1lem4  49683