Theorem unexg 7760

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

Assertion

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

Proof of Theorem unexg

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  Vcvv 3450   ∪ cun 4149  {cpr 4585  ∪ cuni 4866

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-un 4151  df-sn 4584  df-pr 4586  df-uni 4867

This theorem is used by:  unex  7761  unexb  7763  xpexg  7764  unexd  7768  difex2  7774  difsnexi  7775  eldifpw  7782  pwuncl  7784  ordunpr  7837  soex  7933  fnse  8150  suppun  8201  tposexg  8257  frrlem13  8316  tfrlem12  8397  tfrlem16  8401  elmapresaun  8908  ralxpmap  8924  undifixp  8962  undom  9084  domunsncan  9096  domssex2  9156  domssex  9157  sbthfilem  9213  fsuppunbi  9381  elfiun  9422  brwdom2  9567  unwdomg  9578  hfunOLD  9919  setrec1lem4  9971  djuex  9989  djuexALT  10003  alephprc  10178  djudoml  10263  infunabs  10284  fin23lem11  10395  axdc2lem  10526  ttukeylem1  10587  fpwwe2lem12  10727  wunex2  10823  wuncval2  10832  hashunx  14530  hashf1lem1  14600  trclexlem  15147  trclun  15167  relexp0g  15175  relexpsucnnr  15178  isstruct2  17327  setsvalg  17344  setsid  17385  yonffth  18458  pwmndgplus  19141  dmdprdsplit2  20262  basdif0  23271  fiuncmp  23722  refun0  23834  ptbasfi  23900  dfac14lem  23936  ptrescn  23958  xkoptsub  23973  filconn  24202  isufil2  24227  ufileu  24238  filufint  24239  fmfnfmlem4  24276  fmfnfm  24277  fclsfnflim  24346  flimfnfcls  24347  ptcmplem1  24371  elply2  26514  plyss  26517  noeta2  28147  etaslts2  28180  cutbdaybnd2lim  28183  wlkp1lem4  30255  resf1o  33322  tocycfv  33670  tocycf  33678  locfinref  34473  esumsplit  34685  esumpad2  34688  sseqval  35020  bnj1149  35422  tz9.1regs  35802  satfvsuc  36126  satf0suclem  36140  sat1el2xp  36144  fmlasuc0  36149  altxpexg  36743  refssfne  37146  topjoin  37153  weiunse  37256  ttcsnexg  37308  bj-2uplex  37935  ptrest  38538  poimirlem3  38542  paddval  40856  evlselvlem  43617  elrfi  43705  rtrclexlem  44616  clcnvlem  44623  cnvrcl0  44625  dfrtrcl5  44629  iunrelexp0  44702  relexpxpmin  44717  brtrclfv2  44727  sge0resplit  47416  sge0split  47419  setsv  48460