Theorem unexg 7688

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

Assertion

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

Proof of Theorem unexg

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  Vcvv 3440   ∪ cun 3899  {cpr 4582  ∪ cuni 4863

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 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-sn 4581  df-pr 4583  df-uni 4864

This theorem is referenced by:  unex  7689  unexb  7692  xpexg  7695  unexd  7699  difex2  7705  difsnexi  7706  eldifpw  7713  pwuncl  7715  ordunpr  7768  soex  7863  fnse  8075  suppun  8126  tposexg  8182  frrlem13  8240  tfrlem12  8320  tfrlem16  8324  elmapresaun  8818  ralxpmap  8834  undifixp  8872  undom  8993  domunsncan  9005  domssex2  9065  domssex  9066  mapunen  9074  sbthfilem  9122  fsuppunbi  9292  elfiun  9333  brwdom2  9478  unwdomg  9489  djuex  9820  djuexALT  9834  alephprc  10009  djudoml  10095  infunabs  10116  fin23lem11  10227  axdc2lem  10358  ttukeylem1  10419  fpwwe2lem12  10553  wunex2  10649  wuncval2  10658  hashunx  14309  hashf1lem1  14378  trclexlem  14917  trclun  14937  relexp0g  14945  relexpsucnnr  14948  isstruct2  17076  setsvalg  17093  setsid  17134  yonffth  18207  pwmndgplus  18860  dmdprdsplit2  19977  basdif0  22897  fiuncmp  23348  refun0  23459  ptbasfi  23525  dfac14lem  23561  ptrescn  23583  xkoptsub  23598  filconn  23827  isufil2  23852  ufileu  23863  filufint  23864  fmfnfmlem4  23901  fmfnfm  23902  fclsfnflim  23971  flimfnfcls  23972  ptcmplem1  23996  elply2  26157  plyss  26160  noeta2  27757  etaslts2  27790  cutbdaybnd2lim  27793  wlkp1lem4  29748  resf1o  32809  tocycfv  33191  tocycf  33199  locfinref  33998  esumsplit  34210  esumpad2  34213  sseqval  34545  bnj1149  34948  tz9.1regs  35290  satfvsuc  35555  satf0suclem  35569  sat1el2xp  35573  fmlasuc0  35578  altxpexg  36172  hfun  36372  refssfne  36552  topjoin  36559  weiunse  36662  bj-2uplex  37223  ptrest  37816  poimirlem3  37820  paddval  40054  evlselvlem  42825  elrfi  42932  rtrclexlem  43853  clcnvlem  43860  cnvrcl0  43862  dfrtrcl5  43866  iunrelexp0  43939  relexpxpmin  43954  brtrclfv2  43964  sge0resplit  46646  sge0split  46649  setsv  47620  setrec1lem4  49931