Theorem unexg 7737

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

Assertion

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

Proof of Theorem unexg

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  Vcvv 3459   ∪ cun 3924  {cpr 4603  ∪ cuni 4883

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7729

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-sn 4602  df-pr 4604  df-uni 4884

This theorem is referenced by:  unex  7738  unexb  7741  xpexg  7744  unexd  7748  difex2  7754  difsnexi  7755  eldifpw  7762  pwuncl  7764  ordunpr  7820  soex  7917  fnse  8132  suppun  8183  tposexg  8239  frrlem13  8297  wfrlem15OLD  8337  tfrlem12  8403  tfrlem16  8407  elmapresaun  8894  ralxpmap  8910  undifixp  8948  undom  9073  undomOLD  9074  domunsncan  9086  domssex2  9151  domssex  9152  mapunen  9160  sbthfilem  9212  fsuppunbi  9401  elfiun  9442  brwdom2  9587  unwdomg  9598  djuex  9922  djuexALT  9936  alephprc  10113  djudoml  10199  infunabs  10220  fin23lem11  10331  axdc2lem  10462  ttukeylem1  10523  fpwwe2lem12  10656  wunex2  10752  wuncval2  10761  hashunx  14404  hashf1lem1  14473  trclexlem  15013  trclun  15033  relexp0g  15041  relexpsucnnr  15044  isstruct2  17168  setsvalg  17185  setsid  17226  yonffth  18296  pwmndgplus  18913  dmdprdsplit2  20029  basdif0  22891  fiuncmp  23342  refun0  23453  ptbasfi  23519  dfac14lem  23555  ptrescn  23577  xkoptsub  23592  filconn  23821  isufil2  23846  ufileu  23857  filufint  23858  fmfnfmlem4  23895  fmfnfm  23896  fclsfnflim  23965  flimfnfcls  23966  ptcmplem1  23990  elply2  26153  plyss  26156  noeta2  27748  etasslt2  27778  scutbdaybnd2lim  27781  wlkp1lem4  29656  resf1o  32707  tocycfv  33120  tocycf  33128  locfinref  33872  esumsplit  34084  esumpad2  34087  sseqval  34420  bnj1149  34823  satfvsuc  35383  satf0suclem  35397  sat1el2xp  35401  fmlasuc0  35406  altxpexg  35996  hfun  36196  refssfne  36376  topjoin  36383  weiunse  36486  bj-2uplex  37040  ptrest  37643  poimirlem3  37647  paddval  39817  evlselvlem  42609  elrfi  42717  rtrclexlem  43640  clcnvlem  43647  cnvrcl0  43649  dfrtrcl5  43653  iunrelexp0  43726  relexpxpmin  43741  brtrclfv2  43751  sge0resplit  46435  sge0split  46438  setsv  47392  setrec1lem4  49554