Theorem unexg 7589

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 3447	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		elex 3447	. 2 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V)
3		unexb 7588	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ∪ 𝐵) ∈ V)
4	3	biimpi 215	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ∪ 𝐵) ∈ V)
5	1, 2, 4	syl2an 596	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  Vcvv 3429   ∪ cun 3884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5221  ax-nul 5228  ax-pr 5350  ax-un 7578

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3431  df-dif 3889  df-un 3891  df-in 3893  df-ss 3903  df-nul 4257  df-sn 4562  df-pr 4564  df-uni 4840

This theorem is referenced by:  xpexg  7590  unexd  7594  difex2  7600  difsnexi  7601  eldifpw  7608  pwuncl  7610  ordunpr  7663  soex  7758  fnse  7961  suppun  7987  tposexg  8043  frrlem13  8101  wfrlem15OLD  8141  tfrlem12  8207  tfrlem16  8211  elmapresaun  8655  ralxpmap  8671  undifixp  8709  undom  8833  undomOLD  8834  domunsncan  8846  domssex2  8911  domssex  8912  mapunen  8920  sbthfilem  8971  fsuppunbi  9136  elfiun  9176  brwdom2  9319  unwdomg  9330  djuex  9676  djuexALT  9690  alephprc  9865  djudoml  9950  infunabs  9973  fin23lem11  10083  axdc2lem  10214  ttukeylem1  10275  fpwwe2lem12  10408  wunex2  10504  wuncval2  10513  hashunx  14111  hashf1lem1  14178  hashf1lem1OLD  14179  trclexlem  14715  trclun  14735  relexp0g  14743  relexpsucnnr  14746  isstruct2  16860  setsvalg  16877  setsid  16919  yonffth  18012  pwmndgplus  18584  dmdprdsplit2  19659  basdif0  22113  fiuncmp  22565  refun0  22676  ptbasfi  22742  dfac14lem  22778  ptrescn  22800  xkoptsub  22815  filconn  23044  isufil2  23069  ufileu  23080  filufint  23081  fmfnfmlem4  23118  fmfnfm  23119  fclsfnflim  23188  flimfnfcls  23189  ptcmplem1  23213  elply2  25367  plyss  25370  wlkp1lem4  28053  resf1o  31073  tocycfv  31384  tocycf  31392  locfinref  31799  esumsplit  32029  esumpad2  32032  sseqval  32363  bnj1149  32780  satfvsuc  33331  satf0suclem  33345  sat1el2xp  33349  fmlasuc0  33354  noeta2  33987  etasslt2  34016  scutbdaybnd2lim  34019  altxpexg  34288  hfun  34488  refssfne  34555  topjoin  34562  bj-2uplex  35220  ptrest  35784  poimirlem3  35788  paddval  37820  elrfi  40524  rclexi  41204  rtrclexlem  41205  trclubgNEW  41207  clcnvlem  41212  cnvrcl0  41214  dfrtrcl5  41218  iunrelexp0  41291  relexpmulg  41299  relexp01min  41302  relexpxpmin  41306  brtrclfv2  41316  sge0resplit  43925  sge0split  43928  setsv  44808  setrec1lem4  46374