Theorem unexg 4402

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2128  Vcvv 2712   ∪ cun 3100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pr 4169  ax-un 4393

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-rex 2441  df-v 2714  df-un 3106  df-in 3108  df-ss 3115  df-sn 3566  df-pr 3567  df-uni 3773

This theorem is referenced by:  tpexg  4403  eldifpw  4436  ifelpwung  4440  xpexg  4699  tposexg  6202  tfrlemisucaccv  6269  tfrlemibxssdm  6271  tfrlemibfn  6272  tfr1onlemsucaccv  6285  tfr1onlembxssdm  6287  tfr1onlembfn  6288  tfrcllemsucaccv  6298  tfrcllembxssdm  6300  tfrcllembfn  6301  rdgtfr  6318  rdgruledefgg  6319  rdgivallem  6325  djuex  6981  zfz1isolem1  10704  ennnfonelemp1  12118  setsvalg  12191  setsex  12193  setsslid  12211  strleund  12249