Theorem unexg 7690

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

Assertion

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

Proof of Theorem unexg

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  Vcvv 3430   ∪ cun 3888  {cpr 4570  ∪ cuni 4851

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 2709  ax-sep 5231  ax-pr 5370  ax-un 7682

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 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-ss 3907  df-sn 4569  df-pr 4571  df-uni 4852

This theorem is referenced by:  unex  7691  unexb  7694  xpexg  7697  unexd  7701  difex2  7707  difsnexi  7708  eldifpw  7715  pwuncl  7717  ordunpr  7770  soex  7865  fnse  8076  suppun  8127  tposexg  8183  frrlem13  8241  tfrlem12  8321  tfrlem16  8325  elmapresaun  8821  ralxpmap  8837  undifixp  8875  undom  8996  domunsncan  9008  domssex2  9068  domssex  9069  mapunen  9077  sbthfilem  9125  fsuppunbi  9295  elfiun  9336  brwdom2  9481  unwdomg  9492  djuex  9823  djuexALT  9837  alephprc  10012  djudoml  10098  infunabs  10119  fin23lem11  10230  axdc2lem  10361  ttukeylem1  10422  fpwwe2lem12  10556  wunex2  10652  wuncval2  10661  hashunx  14339  hashf1lem1  14408  trclexlem  14947  trclun  14967  relexp0g  14975  relexpsucnnr  14978  isstruct2  17110  setsvalg  17127  setsid  17168  yonffth  18241  pwmndgplus  18897  dmdprdsplit2  20014  basdif0  22928  fiuncmp  23379  refun0  23490  ptbasfi  23556  dfac14lem  23592  ptrescn  23614  xkoptsub  23629  filconn  23858  isufil2  23883  ufileu  23894  filufint  23895  fmfnfmlem4  23932  fmfnfm  23933  fclsfnflim  24002  flimfnfcls  24003  ptcmplem1  24027  elply2  26171  plyss  26174  noeta2  27767  etaslts2  27800  cutbdaybnd2lim  27803  wlkp1lem4  29758  resf1o  32818  tocycfv  33185  tocycf  33193  locfinref  34001  esumsplit  34213  esumpad2  34216  sseqval  34548  bnj1149  34950  tz9.1regs  35294  satfvsuc  35559  satf0suclem  35573  sat1el2xp  35577  fmlasuc0  35582  altxpexg  36176  hfun  36376  refssfne  36556  topjoin  36563  weiunse  36666  ttcsnexg  36718  bj-2uplex  37345  ptrest  37954  poimirlem3  37958  paddval  40258  evlselvlem  43033  elrfi  43140  rtrclexlem  44061  clcnvlem  44068  cnvrcl0  44070  dfrtrcl5  44074  iunrelexp0  44147  relexpxpmin  44162  brtrclfv2  44172  sge0resplit  46852  sge0split  46855  setsv  47850  setrec1lem4  50177