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 2832	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  Vcvv 3436   ∪ cun 3895  {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 2113  ax-9 2121  ax-ext 2703  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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  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  8984  domunsncan  8996  domssex2  9056  domssex  9057  mapunen  9065  sbthfilem  9113  fsuppunbi  9279  elfiun  9320  brwdom2  9465  unwdomg  9476  djuex  9807  djuexALT  9821  alephprc  9996  djudoml  10082  infunabs  10103  fin23lem11  10214  axdc2lem  10345  ttukeylem1  10406  fpwwe2lem12  10539  wunex2  10635  wuncval2  10644  hashunx  14299  hashf1lem1  14368  trclexlem  14907  trclun  14927  relexp0g  14935  relexpsucnnr  14938  isstruct2  17066  setsvalg  17083  setsid  17124  yonffth  18196  pwmndgplus  18849  dmdprdsplit2  19966  basdif0  22874  fiuncmp  23325  refun0  23436  ptbasfi  23502  dfac14lem  23538  ptrescn  23560  xkoptsub  23575  filconn  23804  isufil2  23829  ufileu  23840  filufint  23841  fmfnfmlem4  23878  fmfnfm  23879  fclsfnflim  23948  flimfnfcls  23949  ptcmplem1  23973  elply2  26134  plyss  26137  noeta2  27730  etasslt2  27761  scutbdaybnd2lim  27764  wlkp1lem4  29660  resf1o  32720  tocycfv  33085  tocycf  33093  locfinref  33861  esumsplit  34073  esumpad2  34076  sseqval  34408  bnj1149  34811  tz9.1regs  35137  satfvsuc  35412  satf0suclem  35426  sat1el2xp  35430  fmlasuc0  35435  altxpexg  36029  hfun  36229  refssfne  36409  topjoin  36416  weiunse  36519  bj-2uplex  37073  ptrest  37665  poimirlem3  37669  paddval  39903  evlselvlem  42685  elrfi  42792  rtrclexlem  43714  clcnvlem  43721  cnvrcl0  43723  dfrtrcl5  43727  iunrelexp0  43800  relexpxpmin  43815  brtrclfv2  43825  sge0resplit  46509  sge0split  46512  setsv  47483  setrec1lem4  49796