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 4883	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵))
2		prex 5396	. . . 4 ⊢ {𝐴, 𝐵} ∈ V
3	2	a1i 11	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)
4	3	uniexd 7748	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ {𝐴, 𝐵} ∈ V)
5	1, 4	eqeltrrd 2862	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  Vcvv 3451   ∪ cun 3897  {cpr 4586  ∪ cuni 4867

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 2733  ax-sep 5249  ax-pr 5391  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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916  df-sn 4585  df-pr 4587  df-uni 4868

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  8134  suppun  8185  tposexg  8241  frrlem13  8300  tfrlem12  8381  tfrlem16  8385  elmapresaun  8892  ralxpmap  8908  undifixp  8946  undom  9068  domunsncan  9080  domssex2  9140  domssex  9141  sbthfilem  9197  fsuppunbi  9365  elfiun  9406  brwdom2  9551  unwdomg  9562  hfunOLD  9900  setrec1lem4  9952  djuex  9970  djuexALT  9984  alephprc  10159  djudoml  10244  infunabs  10265  fin23lem11  10376  axdc2lem  10507  ttukeylem1  10568  fpwwe2lem12  10708  wunex2  10804  wuncval2  10813  hashunx  14510  hashf1lem1  14580  trclexlem  15127  trclun  15147  relexp0g  15155  relexpsucnnr  15158  isstruct2  17307  setsvalg  17324  setsid  17365  yonffth  18438  pwmndgplus  19121  dmdprdsplit2  20242  basdif0  23251  fiuncmp  23702  refun0  23814  ptbasfi  23880  dfac14lem  23916  ptrescn  23938  xkoptsub  23953  filconn  24182  isufil2  24207  ufileu  24218  filufint  24219  fmfnfmlem4  24256  fmfnfm  24257  fclsfnflim  24326  flimfnfcls  24327  ptcmplem1  24351  elply2  26494  plyss  26497  noeta2  28129  etaslts2  28162  cutbdaybnd2lim  28165  wlkp1lem4  30237  resf1o  33304  tocycfv  33652  tocycf  33660  locfinref  34455  esumsplit  34667  esumpad2  34670  sseqval  35003  bnj1149  35405  tz9.1regs  35775  satfvsuc  36095  satf0suclem  36109  sat1el2xp  36113  fmlasuc0  36118  altxpexg  36713  refssfne  37116  topjoin  37123  weiunse  37226  ttcsnexg  37278  bj-2uplex  37905  ptrest  38505  poimirlem3  38509  paddval  40823  evlselvlem  43578  elrfi  43658  rtrclexlem  44575  clcnvlem  44582  cnvrcl0  44584  dfrtrcl5  44588  iunrelexp0  44661  relexpxpmin  44676  brtrclfv2  44686  sge0resplit  47360  sge0split  47363  setsv  48404