Theorem unexg 7743

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

Assertion

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

Proof of Theorem unexg

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  Vcvv 3455   ∪ cun 3904  {cpr 4592  ∪ cuni 4873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-ss 3923  df-sn 4591  df-pr 4593  df-uni 4874

This theorem is referenced by:  unex  7744  unexb  7747  xpexg  7750  unexd  7754  difex2  7760  difsnexi  7761  eldifpw  7768  pwuncl  7770  ordunpr  7823  soex  7919  fnse  8130  suppun  8181  tposexg  8237  frrlem13  8296  tfrlem12  8377  tfrlem16  8381  elmapresaun  8879  ralxpmap  8895  undifixp  8933  undom  9054  domunsncan  9066  domssex2  9126  domssex  9127  sbthfilem  9183  fsuppunbi  9350  elfiun  9391  brwdom2  9536  unwdomg  9547  djuex  9895  djuexALT  9909  alephprc  10084  djudoml  10169  infunabs  10190  fin23lem11  10302  axdc2lem  10433  ttukeylem1  10494  fpwwe2lem12  10628  wunex2  10724  wuncval2  10733  hashunx  14424  hashf1lem1  14494  trclexlem  15033  trclun  15053  relexp0g  15061  relexpsucnnr  15064  isstruct2  17210  setsvalg  17227  setsid  17268  yonffth  18341  pwmndgplus  18998  dmdprdsplit2  20119  basdif0  23091  fiuncmp  23542  refun0  23653  ptbasfi  23719  dfac14lem  23755  ptrescn  23777  xkoptsub  23792  filconn  24021  isufil2  24046  ufileu  24057  filufint  24058  fmfnfmlem4  24095  fmfnfm  24096  fclsfnflim  24165  flimfnfcls  24166  ptcmplem1  24190  elply2  26334  plyss  26337  noeta2  27935  etaslts2  27968  cutbdaybnd2lim  27971  wlkp1lem4  30005  resf1o  33056  tocycfv  33410  tocycf  33418  locfinref  34212  esumsplit  34424  esumpad2  34427  sseqval  34759  bnj1149  35161  tz9.1regs  35528  satfvsuc  35834  satf0suclem  35848  sat1el2xp  35852  fmlasuc0  35857  altxpexg  36451  hfun  36651  refssfne  36850  topjoin  36857  weiunse  36960  ttcsnexg  37012  bj-2uplex  37639  ptrest  38251  poimirlem3  38255  paddval  40553  evlselvlem  43303  elrfi  43408  rtrclexlem  44325  clcnvlem  44332  cnvrcl0  44334  dfrtrcl5  44338  iunrelexp0  44411  relexpxpmin  44426  brtrclfv2  44436  sge0resplit  47103  sge0split  47106  setsv  48110  setrec1lem4  50451