Theorem unexg 7577

Description: A union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 18-Sep-2006.)

Assertion

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

Proof of Theorem unexg

Step	Hyp	Ref	Expression
1		elex 3440	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		elex 3440	. 2 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V)
3		unexb 7576	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ∪ 𝐵) ∈ V)
4	3	biimpi 215	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ∪ 𝐵) ∈ V)
5	1, 2, 4	syl2an 595	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  Vcvv 3422   ∪ cun 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-sn 4559  df-pr 4561  df-uni 4837

This theorem is referenced by:  xpexg  7578  unexd  7582  difex2  7588  difsnexi  7589  eldifpw  7596  pwuncl  7598  ordunpr  7648  soex  7742  fnse  7945  suppun  7971  tposexg  8027  frrlem13  8085  wfrlem15OLD  8125  tfrlem12  8191  tfrlem16  8195  elmapresaun  8626  ralxpmap  8642  undifixp  8680  undom  8800  domunsncan  8812  domssex2  8873  domssex  8874  mapunen  8882  sbthfilem  8941  fsuppunbi  9079  elfiun  9119  brwdom2  9262  unwdomg  9273  djuex  9597  djuexALT  9611  alephprc  9786  djudoml  9871  infunabs  9894  fin23lem11  10004  axdc2lem  10135  ttukeylem1  10196  fpwwe2lem12  10329  wunex2  10425  wuncval2  10434  hashunx  14029  hashf1lem1  14096  hashf1lem1OLD  14097  trclexlem  14633  trclun  14653  relexp0g  14661  relexpsucnnr  14664  isstruct2  16778  setsvalg  16795  setsid  16837  yonffth  17918  pwmndgplus  18489  dmdprdsplit2  19564  basdif0  22011  fiuncmp  22463  refun0  22574  ptbasfi  22640  dfac14lem  22676  ptrescn  22698  xkoptsub  22713  filconn  22942  isufil2  22967  ufileu  22978  filufint  22979  fmfnfmlem4  23016  fmfnfm  23017  fclsfnflim  23086  flimfnfcls  23087  ptcmplem1  23111  elply2  25262  plyss  25265  wlkp1lem4  27946  resf1o  30967  tocycfv  31278  tocycf  31286  locfinref  31693  esumsplit  31921  esumpad2  31924  sseqval  32255  bnj1149  32672  satfvsuc  33223  satf0suclem  33237  sat1el2xp  33241  fmlasuc0  33246  noeta2  33906  etasslt2  33935  scutbdaybnd2lim  33938  altxpexg  34207  hfun  34407  refssfne  34474  topjoin  34481  bj-2uplex  35139  ptrest  35703  poimirlem3  35707  paddval  37739  elrfi  40432  rclexi  41112  rtrclexlem  41113  trclubgNEW  41115  clcnvlem  41120  cnvrcl0  41122  dfrtrcl5  41126  iunrelexp0  41199  relexpmulg  41207  relexp01min  41210  relexpxpmin  41214  brtrclfv2  41224  sge0resplit  43834  sge0split  43837  setsv  44718  setrec1lem4  46282