Theorem unexg 7761

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

Assertion

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

Proof of Theorem unexg

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  Vcvv 3477   ∪ cun 3960  {cpr 4632  ∪ cuni 4911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-sn 4631  df-pr 4633  df-uni 4912

This theorem is referenced by:  unex  7762  unexb  7765  xpexg  7768  unexd  7772  difex2  7778  difsnexi  7779  eldifpw  7786  pwuncl  7788  ordunpr  7845  soex  7943  fnse  8156  suppun  8207  tposexg  8263  frrlem13  8321  wfrlem15OLD  8361  tfrlem12  8427  tfrlem16  8431  elmapresaun  8918  ralxpmap  8934  undifixp  8972  undom  9097  undomOLD  9098  domunsncan  9110  domssex2  9175  domssex  9176  mapunen  9184  sbthfilem  9235  fsuppunbi  9426  elfiun  9467  brwdom2  9610  unwdomg  9621  djuex  9945  djuexALT  9959  alephprc  10136  djudoml  10222  infunabs  10243  fin23lem11  10354  axdc2lem  10485  ttukeylem1  10546  fpwwe2lem12  10679  wunex2  10775  wuncval2  10784  hashunx  14421  hashf1lem1  14490  trclexlem  15029  trclun  15049  relexp0g  15057  relexpsucnnr  15060  isstruct2  17182  setsvalg  17199  setsid  17241  yonffth  18340  pwmndgplus  18960  dmdprdsplit2  20080  basdif0  22975  fiuncmp  23427  refun0  23538  ptbasfi  23604  dfac14lem  23640  ptrescn  23662  xkoptsub  23677  filconn  23906  isufil2  23931  ufileu  23942  filufint  23943  fmfnfmlem4  23980  fmfnfm  23981  fclsfnflim  24050  flimfnfcls  24051  ptcmplem1  24075  elply2  26249  plyss  26252  noeta2  27843  etasslt2  27873  scutbdaybnd2lim  27876  wlkp1lem4  29708  resf1o  32747  tocycfv  33111  tocycf  33119  locfinref  33801  esumsplit  34033  esumpad2  34036  sseqval  34369  bnj1149  34784  satfvsuc  35345  satf0suclem  35359  sat1el2xp  35363  fmlasuc0  35368  altxpexg  35959  hfun  36159  refssfne  36340  topjoin  36347  weiunse  36450  bj-2uplex  37004  ptrest  37605  poimirlem3  37609  paddval  39780  evlselvlem  42572  elrfi  42681  rtrclexlem  43605  clcnvlem  43612  cnvrcl0  43614  dfrtrcl5  43618  iunrelexp0  43691  relexpxpmin  43706  brtrclfv2  43716  sge0resplit  46361  sge0split  46364  setsv  47302  setrec1lem4  48920