Theorem unexg 7787

Description: The union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 18-Sep-2006.) Prove unexg 7787 first and then unex 7788 and unexb 7790 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 5401	. . . 4 ⊢ {𝐴, 𝐵} ∈ V
3	2	a1i 11	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)
4	3	uniexd 7786	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ {𝐴, 𝐵} ∈ V)
5	1, 4	eqeltrrd 2865	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  Vcvv 3454   ∪ cun 4152  {cpr 4590  ∪ 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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-pr 5396  ax-un 7778

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-sn 4589  df-pr 4591  df-uni 4871

This theorem is used by:  unex  7788  unexb  7790  xpexg  7791  unexd  7795  difex2  7801  difsnexi  7802  eldifpw  7809  pwuncl  7811  ordunpr  7864  soex  7960  fnse  8180  suppun  8232  tposexg  8288  frrlem13  8347  tfrlem12  8428  tfrlem16  8432  elmapresaun  8939  ralxpmap  8955  undifixp  8993  undom  9115  domunsncan  9127  domssex2  9187  domssex  9188  sbthfilem  9244  fsuppunbi  9411  elfiun  9452  brwdom2  9597  unwdomg  9608  hfunOLD  9949  setrec1lem4  10001  djuex  10019  djuexALT  10033  alephprc  10208  djudoml  10293  infunabs  10314  fin23lem11  10425  axdc2lem  10556  ttukeylem1  10617  fpwwe2lem12  10757  wunex2  10853  wuncval2  10862  hashunx  14560  hashf1lem1  14630  trclexlem  15179  trclun  15199  relexp0g  15207  relexpsucnnr  15210  isstruct2  17359  setsvalg  17376  setsid  17417  yonffth  18490  pwmndgplus  19173  dmdprdsplit2  20295  basdif0  23304  fiuncmp  23755  refun0  23867  ptbasfi  23933  dfac14lem  23969  ptrescn  23991  xkoptsub  24006  filconn  24235  isufil2  24260  ufileu  24271  filufint  24272  fmfnfmlem4  24309  fmfnfm  24310  fclsfnflim  24379  flimfnfcls  24380  ptcmplem1  24404  elply2  26547  plyss  26550  etaslts2  28213  cutbdaybnd2lim  28216  wlkp1lem4  30288  resf1o  33395  tocycfv  33746  tocycf  33754  locfinref  34556  esumsplit  34768  esumpad2  34771  sseqval  35103  bnj1149  35505  tz9.1regs  35915  satfvsuc  36306  satf0suclem  36320  sat1el2xp  36324  fmlasuc0  36329  altxpexg  36934  refssfne  37337  topjoin  37344  weiunse  37447  ttcsnexg  37499  bj-2uplex  38126  ptrest  38742  poimirlem3  38746  paddval  41058  evlselvlem  43820  elrfi  43909  rtrclexlem  44819  clcnvlem  44826  cnvrcl0  44828  dfrtrcl5  44832  iunrelexp0  44905  relexpxpmin  44920  brtrclfv2  44930  sge0resplit  47631  sge0split  47634  setsv  48675