Theorem unexg 7693

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

Assertion

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

Proof of Theorem unexg

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  Vcvv 3432   ∪ cun 3888  {cpr 4564  ∪ cuni 4845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-ss 3907  df-sn 4563  df-pr 4565  df-uni 4846

This theorem is referenced by:  unex  7694  unexb  7697  xpexg  7700  unexd  7704  difex2  7710  difsnexi  7711  eldifpw  7718  pwuncl  7720  ordunpr  7773  soex  7868  fnse  8080  suppun  8131  tposexg  8187  frrlem13  8245  tfrlem12  8325  tfrlem16  8329  elmapresaun  8825  ralxpmap  8841  undifixp  8879  undom  9000  domunsncan  9012  domssex2  9072  domssex  9073  sbthfilem  9129  fsuppunbi  9299  elfiun  9340  brwdom2  9485  unwdomg  9496  djuex  9830  djuexALT  9844  alephprc  10019  djudoml  10105  infunabs  10126  fin23lem11  10237  axdc2lem  10368  ttukeylem1  10429  fpwwe2lem12  10563  wunex2  10659  wuncval2  10668  hashunx  14346  hashf1lem1  14415  trclexlem  14954  trclun  14974  relexp0g  14982  relexpsucnnr  14985  isstruct2  17117  setsvalg  17134  setsid  17175  yonffth  18248  pwmndgplus  18904  dmdprdsplit2  20021  basdif0  22943  fiuncmp  23394  refun0  23505  ptbasfi  23571  dfac14lem  23607  ptrescn  23629  xkoptsub  23644  filconn  23873  isufil2  23898  ufileu  23909  filufint  23910  fmfnfmlem4  23947  fmfnfm  23948  fclsfnflim  24017  flimfnfcls  24018  ptcmplem1  24042  elply2  26186  plyss  26189  noeta2  27778  etaslts2  27811  cutbdaybnd2lim  27814  wlkp1lem4  29768  resf1o  32829  tocycfv  33197  tocycf  33205  locfinref  34032  esumsplit  34244  esumpad2  34247  sseqval  34579  bnj1149  34981  tz9.1regs  35322  satfvsuc  35596  satf0suclem  35610  sat1el2xp  35614  fmlasuc0  35619  altxpexg  36213  hfun  36413  refssfne  36593  topjoin  36600  weiunse  36703  ttcsnexg  36755  bj-2uplex  37382  ptrest  37993  poimirlem3  37997  paddval  40297  evlselvlem  43045  elrfi  43150  rtrclexlem  44067  clcnvlem  44074  cnvrcl0  44076  dfrtrcl5  44080  iunrelexp0  44153  relexpxpmin  44168  brtrclfv2  44178  sge0resplit  46856  sge0split  46859  setsv  47860  setrec1lem4  50187