Theorem unexg 7763

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

Assertion

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

Proof of Theorem unexg

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  Vcvv 3480   ∪ cun 3949  {cpr 4628  ∪ cuni 4907

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 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-sn 4627  df-pr 4629  df-uni 4908

This theorem is referenced by:  unex  7764  unexb  7767  xpexg  7770  unexd  7774  difex2  7780  difsnexi  7781  eldifpw  7788  pwuncl  7790  ordunpr  7846  soex  7943  fnse  8158  suppun  8209  tposexg  8265  frrlem13  8323  wfrlem15OLD  8363  tfrlem12  8429  tfrlem16  8433  elmapresaun  8920  ralxpmap  8936  undifixp  8974  undom  9099  undomOLD  9100  domunsncan  9112  domssex2  9177  domssex  9178  mapunen  9186  sbthfilem  9238  fsuppunbi  9429  elfiun  9470  brwdom2  9613  unwdomg  9624  djuex  9948  djuexALT  9962  alephprc  10139  djudoml  10225  infunabs  10246  fin23lem11  10357  axdc2lem  10488  ttukeylem1  10549  fpwwe2lem12  10682  wunex2  10778  wuncval2  10787  hashunx  14425  hashf1lem1  14494  trclexlem  15033  trclun  15053  relexp0g  15061  relexpsucnnr  15064  isstruct2  17186  setsvalg  17203  setsid  17244  yonffth  18329  pwmndgplus  18948  dmdprdsplit2  20066  basdif0  22960  fiuncmp  23412  refun0  23523  ptbasfi  23589  dfac14lem  23625  ptrescn  23647  xkoptsub  23662  filconn  23891  isufil2  23916  ufileu  23927  filufint  23928  fmfnfmlem4  23965  fmfnfm  23966  fclsfnflim  24035  flimfnfcls  24036  ptcmplem1  24060  elply2  26235  plyss  26238  noeta2  27829  etasslt2  27859  scutbdaybnd2lim  27862  wlkp1lem4  29694  resf1o  32741  tocycfv  33129  tocycf  33137  locfinref  33840  esumsplit  34054  esumpad2  34057  sseqval  34390  bnj1149  34806  satfvsuc  35366  satf0suclem  35380  sat1el2xp  35384  fmlasuc0  35389  altxpexg  35979  hfun  36179  refssfne  36359  topjoin  36366  weiunse  36469  bj-2uplex  37023  ptrest  37626  poimirlem3  37630  paddval  39800  evlselvlem  42596  elrfi  42705  rtrclexlem  43629  clcnvlem  43636  cnvrcl0  43638  dfrtrcl5  43642  iunrelexp0  43715  relexpxpmin  43730  brtrclfv2  43740  sge0resplit  46421  sge0split  46424  setsv  47365  setrec1lem4  49209