Theorem unexg 7760

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

Assertion

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

Proof of Theorem unexg

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  Vcvv 3450   ∪ cun 4149  {cpr 4586  ∪ cuni 4866

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-un 4151  df-sn 4585  df-pr 4587  df-uni 4867

This theorem is used by:  unex  7761  unexb  7763  xpexg  7764  unexd  7768  difex2  7774  difsnexi  7775  eldifpw  7782  pwuncl  7784  ordunpr  7837  soex  7933  fnse  8152  suppun  8204  tposexg  8260  frrlem13  8319  tfrlem12  8400  tfrlem16  8404  elmapresaun  8911  ralxpmap  8927  undifixp  8965  undom  9087  domunsncan  9099  domssex2  9159  domssex  9160  sbthfilem  9216  fsuppunbi  9384  elfiun  9425  brwdom2  9570  unwdomg  9581  hfunOLD  9922  setrec1lem4  9974  djuex  9992  djuexALT  10006  alephprc  10181  djudoml  10266  infunabs  10287  fin23lem11  10398  axdc2lem  10529  ttukeylem1  10590  fpwwe2lem12  10730  wunex2  10826  wuncval2  10835  hashunx  14533  hashf1lem1  14603  trclexlem  15152  trclun  15172  relexp0g  15180  relexpsucnnr  15183  isstruct2  17332  setsvalg  17349  setsid  17390  yonffth  18463  pwmndgplus  19146  dmdprdsplit2  20267  basdif0  23276  fiuncmp  23727  refun0  23839  ptbasfi  23905  dfac14lem  23941  ptrescn  23963  xkoptsub  23978  filconn  24207  isufil2  24232  ufileu  24243  filufint  24244  fmfnfmlem4  24281  fmfnfm  24282  fclsfnflim  24351  flimfnfcls  24352  ptcmplem1  24376  elply2  26519  plyss  26522  etaslts2  28185  cutbdaybnd2lim  28188  wlkp1lem4  30260  resf1o  33368  tocycfv  33716  tocycf  33724  locfinref  34519  esumsplit  34731  esumpad2  34734  sseqval  35066  bnj1149  35468  tz9.1regs  35858  satfvsuc  36212  satf0suclem  36226  sat1el2xp  36230  fmlasuc0  36235  altxpexg  36835  refssfne  37238  topjoin  37245  weiunse  37348  ttcsnexg  37400  bj-2uplex  38027  ptrest  38630  poimirlem3  38634  paddval  40948  evlselvlem  43709  elrfi  43798  rtrclexlem  44709  clcnvlem  44716  cnvrcl0  44718  dfrtrcl5  44722  iunrelexp0  44795  relexpxpmin  44810  brtrclfv2  44820  sge0resplit  47509  sge0split  47512  setsv  48553