Theorem unexg 7778

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

Assertion

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

Proof of Theorem unexg

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  Vcvv 3488   ∪ cun 3974  {cpr 4650  ∪ cuni 4931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-sn 4649  df-pr 4651  df-uni 4932

This theorem is referenced by:  unex  7779  unexb  7782  xpexg  7785  unexd  7789  difex2  7795  difsnexi  7796  eldifpw  7803  pwuncl  7805  ordunpr  7862  soex  7961  fnse  8174  suppun  8225  tposexg  8281  frrlem13  8339  wfrlem15OLD  8379  tfrlem12  8445  tfrlem16  8449  elmapresaun  8938  ralxpmap  8954  undifixp  8992  undom  9125  undomOLD  9126  domunsncan  9138  domssex2  9203  domssex  9204  mapunen  9212  sbthfilem  9264  fsuppunbi  9458  elfiun  9499  brwdom2  9642  unwdomg  9653  djuex  9977  djuexALT  9991  alephprc  10168  djudoml  10254  infunabs  10275  fin23lem11  10386  axdc2lem  10517  ttukeylem1  10578  fpwwe2lem12  10711  wunex2  10807  wuncval2  10816  hashunx  14435  hashf1lem1  14504  trclexlem  15043  trclun  15063  relexp0g  15071  relexpsucnnr  15074  isstruct2  17196  setsvalg  17213  setsid  17255  yonffth  18354  pwmndgplus  18970  dmdprdsplit2  20090  basdif0  22981  fiuncmp  23433  refun0  23544  ptbasfi  23610  dfac14lem  23646  ptrescn  23668  xkoptsub  23683  filconn  23912  isufil2  23937  ufileu  23948  filufint  23949  fmfnfmlem4  23986  fmfnfm  23987  fclsfnflim  24056  flimfnfcls  24057  ptcmplem1  24081  elply2  26255  plyss  26258  noeta2  27847  etasslt2  27877  scutbdaybnd2lim  27880  wlkp1lem4  29712  resf1o  32744  tocycfv  33102  tocycf  33110  locfinref  33787  esumsplit  34017  esumpad2  34020  sseqval  34353  bnj1149  34768  satfvsuc  35329  satf0suclem  35343  sat1el2xp  35347  fmlasuc0  35352  altxpexg  35942  hfun  36142  refssfne  36324  topjoin  36331  weiunse  36434  bj-2uplex  36988  ptrest  37579  poimirlem3  37583  paddval  39755  evlselvlem  42541  elrfi  42650  rtrclexlem  43578  clcnvlem  43585  cnvrcl0  43587  dfrtrcl5  43591  iunrelexp0  43664  relexpxpmin  43679  brtrclfv2  43689  sge0resplit  46327  sge0split  46330  setsv  47252  setrec1lem4  48782