Theorem unexg 7698

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

Assertion

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

Proof of Theorem unexg

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  Vcvv 3442   ∪ cun 3901  {cpr 4584  ∪ cuni 4865

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 5243  ax-pr 5379  ax-un 7690

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 3444  df-un 3908  df-ss 3920  df-sn 4583  df-pr 4585  df-uni 4866

This theorem is referenced by:  unex  7699  unexb  7702  xpexg  7705  unexd  7709  difex2  7715  difsnexi  7716  eldifpw  7723  pwuncl  7725  ordunpr  7778  soex  7873  fnse  8085  suppun  8136  tposexg  8192  frrlem13  8250  tfrlem12  8330  tfrlem16  8334  elmapresaun  8830  ralxpmap  8846  undifixp  8884  undom  9005  domunsncan  9017  domssex2  9077  domssex  9078  mapunen  9086  sbthfilem  9134  fsuppunbi  9304  elfiun  9345  brwdom2  9490  unwdomg  9501  djuex  9832  djuexALT  9846  alephprc  10021  djudoml  10107  infunabs  10128  fin23lem11  10239  axdc2lem  10370  ttukeylem1  10431  fpwwe2lem12  10565  wunex2  10661  wuncval2  10670  hashunx  14321  hashf1lem1  14390  trclexlem  14929  trclun  14949  relexp0g  14957  relexpsucnnr  14960  isstruct2  17088  setsvalg  17105  setsid  17146  yonffth  18219  pwmndgplus  18872  dmdprdsplit2  19989  basdif0  22909  fiuncmp  23360  refun0  23471  ptbasfi  23537  dfac14lem  23573  ptrescn  23595  xkoptsub  23610  filconn  23839  isufil2  23864  ufileu  23875  filufint  23876  fmfnfmlem4  23913  fmfnfm  23914  fclsfnflim  23983  flimfnfcls  23984  ptcmplem1  24008  elply2  26169  plyss  26172  noeta2  27769  etaslts2  27802  cutbdaybnd2lim  27805  wlkp1lem4  29760  resf1o  32819  tocycfv  33202  tocycf  33210  locfinref  34018  esumsplit  34230  esumpad2  34233  sseqval  34565  bnj1149  34967  tz9.1regs  35309  satfvsuc  35574  satf0suclem  35588  sat1el2xp  35592  fmlasuc0  35597  altxpexg  36191  hfun  36391  refssfne  36571  topjoin  36578  weiunse  36681  bj-2uplex  37264  ptrest  37864  poimirlem3  37868  paddval  40168  evlselvlem  42938  elrfi  43045  rtrclexlem  43966  clcnvlem  43973  cnvrcl0  43975  dfrtrcl5  43979  iunrelexp0  44052  relexpxpmin  44067  brtrclfv2  44077  sge0resplit  46758  sge0split  46761  setsv  47732  setrec1lem4  50043