Theorem unexg 7719

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

Assertion

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

Proof of Theorem unexg

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Vcvv 3447   ∪ cun 3912  {cpr 4591  ∪ cuni 4871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-sn 4590  df-pr 4592  df-uni 4872

This theorem is referenced by:  unex  7720  unexb  7723  xpexg  7726  unexd  7730  difex2  7736  difsnexi  7737  eldifpw  7744  pwuncl  7746  ordunpr  7801  soex  7897  fnse  8112  suppun  8163  tposexg  8219  frrlem13  8277  tfrlem12  8357  tfrlem16  8361  elmapresaun  8853  ralxpmap  8869  undifixp  8907  undom  9029  domunsncan  9041  domssex2  9101  domssex  9102  mapunen  9110  sbthfilem  9162  fsuppunbi  9340  elfiun  9381  brwdom2  9526  unwdomg  9537  djuex  9861  djuexALT  9875  alephprc  10052  djudoml  10138  infunabs  10159  fin23lem11  10270  axdc2lem  10401  ttukeylem1  10462  fpwwe2lem12  10595  wunex2  10691  wuncval2  10700  hashunx  14351  hashf1lem1  14420  trclexlem  14960  trclun  14980  relexp0g  14988  relexpsucnnr  14991  isstruct2  17119  setsvalg  17136  setsid  17177  yonffth  18245  pwmndgplus  18862  dmdprdsplit2  19978  basdif0  22840  fiuncmp  23291  refun0  23402  ptbasfi  23468  dfac14lem  23504  ptrescn  23526  xkoptsub  23541  filconn  23770  isufil2  23795  ufileu  23806  filufint  23807  fmfnfmlem4  23844  fmfnfm  23845  fclsfnflim  23914  flimfnfcls  23915  ptcmplem1  23939  elply2  26101  plyss  26104  noeta2  27696  etasslt2  27726  scutbdaybnd2lim  27729  wlkp1lem4  29604  resf1o  32653  tocycfv  33066  tocycf  33074  locfinref  33831  esumsplit  34043  esumpad2  34046  sseqval  34379  bnj1149  34782  satfvsuc  35348  satf0suclem  35362  sat1el2xp  35366  fmlasuc0  35371  altxpexg  35966  hfun  36166  refssfne  36346  topjoin  36353  weiunse  36456  bj-2uplex  37010  ptrest  37613  poimirlem3  37617  paddval  39792  evlselvlem  42574  elrfi  42682  rtrclexlem  43605  clcnvlem  43612  cnvrcl0  43614  dfrtrcl5  43618  iunrelexp0  43691  relexpxpmin  43706  brtrclfv2  43716  sge0resplit  46404  sge0split  46407  setsv  47379  setrec1lem4  49679