Theorem unexg 7754

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

Assertion

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

Proof of Theorem unexg

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  Vcvv 3458   ∪ cun 3906  {cpr 4596  ∪ cuni 4877

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 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409  ax-un 7745

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 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-ss 3925  df-sn 4595  df-pr 4597  df-uni 4878

This theorem is used by:  unex  7755  unexb  7757  xpexg  7758  unexd  7762  difex2  7768  difsnexi  7769  eldifpw  7776  pwuncl  7778  ordunpr  7831  soex  7927  fnse  8138  suppun  8189  tposexg  8245  frrlem13  8304  tfrlem12  8385  tfrlem16  8389  elmapresaun  8887  ralxpmap  8903  undifixp  8941  undom  9063  domunsncan  9075  domssex2  9135  domssex  9136  sbthfilem  9192  fsuppunbi  9359  elfiun  9400  brwdom2  9545  unwdomg  9556  djuex  9913  djuexALT  9927  alephprc  10102  djudoml  10187  infunabs  10208  fin23lem11  10319  axdc2lem  10450  ttukeylem1  10511  fpwwe2lem12  10645  wunex2  10741  wuncval2  10750  hashunx  14442  hashf1lem1  14512  trclexlem  15057  trclun  15077  relexp0g  15085  relexpsucnnr  15088  isstruct2  17234  setsvalg  17251  setsid  17292  yonffth  18365  pwmndgplus  19028  dmdprdsplit2  20149  basdif0  23147  fiuncmp  23598  refun0  23709  ptbasfi  23775  dfac14lem  23811  ptrescn  23833  xkoptsub  23848  filconn  24077  isufil2  24102  ufileu  24113  filufint  24114  fmfnfmlem4  24151  fmfnfm  24152  fclsfnflim  24221  flimfnfcls  24222  ptcmplem1  24246  elply2  26390  plyss  26393  noeta2  27991  etaslts2  28024  cutbdaybnd2lim  28027  wlkp1lem4  30061  resf1o  33112  tocycfv  33460  tocycf  33468  locfinref  34262  esumsplit  34474  esumpad2  34477  sseqval  34810  bnj1149  35212  tz9.1regs  35571  satfvsuc  35874  satf0suclem  35888  sat1el2xp  35892  fmlasuc0  35897  altxpexg  36491  hfun  36691  refssfne  36910  topjoin  36917  weiunse  37020  ttcsnexg  37072  bj-2uplex  37699  ptrest  38311  poimirlem3  38315  paddval  40613  evlselvlem  43361  elrfi  43466  rtrclexlem  44383  clcnvlem  44390  cnvrcl0  44392  dfrtrcl5  44396  iunrelexp0  44469  relexpxpmin  44484  brtrclfv2  44494  sge0resplit  47161  sge0split  47164  setsv  48168  setrec1lem4  50509