Theorem unexg 7749

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

Assertion

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

Proof of Theorem unexg

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  Vcvv 3453   ∪ cun 3900  {cpr 4589  ∪ cuni 4870

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pr 5402  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-ss 3919  df-sn 4588  df-pr 4590  df-uni 4871

This theorem is used by:  unex  7750  unexb  7752  xpexg  7753  unexd  7757  difex2  7763  difsnexi  7764  eldifpw  7771  pwuncl  7773  ordunpr  7826  soex  7922  fnse  8135  suppun  8186  tposexg  8242  frrlem13  8301  tfrlem12  8382  tfrlem16  8386  elmapresaun  8891  ralxpmap  8907  undifixp  8945  undom  9067  domunsncan  9079  domssex2  9139  domssex  9140  sbthfilem  9196  fsuppunbi  9363  elfiun  9404  brwdom2  9549  unwdomg  9560  djuex  9917  djuexALT  9931  alephprc  10106  djudoml  10191  infunabs  10212  fin23lem11  10323  axdc2lem  10454  ttukeylem1  10515  fpwwe2lem12  10655  wunex2  10751  wuncval2  10760  hashunx  14454  hashf1lem1  14524  trclexlem  15071  trclun  15091  relexp0g  15099  relexpsucnnr  15102  isstruct2  17247  setsvalg  17264  setsid  17305  yonffth  18378  pwmndgplus  19060  dmdprdsplit2  20181  basdif0  23184  fiuncmp  23635  refun0  23747  ptbasfi  23813  dfac14lem  23849  ptrescn  23871  xkoptsub  23886  filconn  24115  isufil2  24140  ufileu  24151  filufint  24152  fmfnfmlem4  24189  fmfnfm  24190  fclsfnflim  24259  flimfnfcls  24260  ptcmplem1  24284  elply2  26428  plyss  26431  noeta2  28034  etaslts2  28067  cutbdaybnd2lim  28070  wlkp1lem4  30142  resf1o  33209  tocycfv  33557  tocycf  33565  locfinref  34359  esumsplit  34571  esumpad2  34574  sseqval  34907  bnj1149  35309  tz9.1regs  35668  satfvsuc  35948  satf0suclem  35962  sat1el2xp  35966  fmlasuc0  35971  altxpexg  36566  hfun  36766  refssfne  36985  topjoin  36992  weiunse  37095  ttcsnexg  37147  bj-2uplex  37774  ptrest  38376  poimirlem3  38380  paddval  40679  evlselvlem  43442  elrfi  43547  rtrclexlem  44464  clcnvlem  44471  cnvrcl0  44473  dfrtrcl5  44477  iunrelexp0  44550  relexpxpmin  44565  brtrclfv2  44575  sge0resplit  47242  sge0split  47245  setsv  48286  setrec1lem4  50624