Theorem unexg 7730

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

Assertion

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

Proof of Theorem unexg

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145  Vcvv 3457   ∪ cun 3905  {cpr 4587  ∪ cuni 4868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5251  ax-pr 5395  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-ss 3924  df-sn 4586  df-pr 4588  df-uni 4869

This theorem is referenced by:  unex  7731  unexb  7734  xpexg  7737  unexd  7741  difex2  7747  difsnexi  7748  eldifpw  7755  pwuncl  7757  ordunpr  7810  soex  7906  fnse  8117  suppun  8168  tposexg  8224  frrlem13  8283  tfrlem12  8364  tfrlem16  8368  elmapresaun  8866  ralxpmap  8882  undifixp  8920  undom  9041  domunsncan  9053  domssex2  9113  domssex  9114  sbthfilem  9170  fsuppunbi  9337  elfiun  9378  brwdom2  9523  unwdomg  9534  djuex  9882  djuexALT  9896  alephprc  10071  djudoml  10156  infunabs  10177  fin23lem11  10289  axdc2lem  10420  ttukeylem1  10481  fpwwe2lem12  10615  wunex2  10711  wuncval2  10720  hashunx  14413  hashf1lem1  14482  trclexlem  15021  trclun  15041  relexp0g  15049  relexpsucnnr  15052  isstruct2  17199  setsvalg  17216  setsid  17257  yonffth  18330  pwmndgplus  18987  dmdprdsplit2  20109  basdif0  23071  fiuncmp  23522  refun0  23633  ptbasfi  23699  dfac14lem  23735  ptrescn  23757  xkoptsub  23772  filconn  24001  isufil2  24026  ufileu  24037  filufint  24038  fmfnfmlem4  24075  fmfnfm  24076  fclsfnflim  24145  flimfnfcls  24146  ptcmplem1  24170  elply2  26314  plyss  26317  noeta2  27912  etaslts2  27945  cutbdaybnd2lim  27948  wlkp1lem4  29933  resf1o  32987  tocycfv  33342  tocycf  33350  locfinref  34148  esumsplit  34360  esumpad2  34363  sseqval  34695  bnj1149  35097  tz9.1regs  35442  satfvsuc  35724  satf0suclem  35738  sat1el2xp  35742  fmlasuc0  35747  altxpexg  36341  hfun  36541  refssfne  36731  topjoin  36738  weiunse  36841  ttcsnexg  36893  bj-2uplex  37519  ptrest  38130  poimirlem3  38134  paddval  40434  evlselvlem  43182  elrfi  43287  rtrclexlem  44204  clcnvlem  44211  cnvrcl0  44213  dfrtrcl5  44217  iunrelexp0  44290  relexpxpmin  44305  brtrclfv2  44315  sge0resplit  46978  sge0split  46981  setsv  47982  setrec1lem4  50319