Theorem unexg 6959

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

Syntax hints:   → wi 4   ∧ wa 384   ∈ wcel 1990  Vcvv 3200   ∪ cun 3572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-sn 4178  df-pr 4180  df-uni 4437

This theorem is referenced by:  xpexg  6960  difex2  6969  difsnexi  6970  eldifpw  6976  ordunpr  7026  soex  7109  fnse  7294  suppun  7315  tposexg  7366  wfrlem15  7429  tfrlem12  7485  tfrlem16  7489  ralxpmap  7907  undifixp  7944  undom  8048  domunsncan  8060  domssex2  8120  domssex  8121  mapunen  8129  fsuppunbi  8296  elfiun  8336  brwdom2  8478  unwdomg  8489  alephprc  8922  cdadom3  9010  infunabs  9029  fin23lem11  9139  axdc2lem  9270  ttukeylem1  9331  fpwwe2lem13  9464  wunex2  9560  wuncval2  9569  hashunx  13175  hashf1lem1  13239  trclexlem  13733  trclun  13755  relexp0g  13762  relexpsucnnr  13765  isstruct2  15867  setsvalg  15887  setsid  15914  yonffth  16924  dmdprdsplit2  18445  basdif0  20757  fiuncmp  21207  refun0  21318  ptbasfi  21384  dfac14lem  21420  ptrescn  21442  xkoptsub  21457  filconn  21687  isufil2  21712  ufileu  21723  filufint  21724  fmfnfmlem4  21761  fmfnfm  21762  fclsfnflim  21831  flimfnfcls  21832  ptcmplem1  21856  elply2  23952  plyss  23955  wlkp1lem4  26573  resf1o  29505  locfinref  29908  esumsplit  30115  esumpad2  30118  sseqval  30450  bnj1149  30863  ssltun1  31915  ssltun2  31916  altxpexg  32085  hfun  32285  refssfne  32353  topjoin  32360  bj-2uplex  33010  ptrest  33408  poimirlem3  33412  paddval  35084  elrfi  37257  elmapresaun  37334  rclexi  37922  rtrclexlem  37923  trclubgNEW  37925  clcnvlem  37930  cnvrcl0  37932  dfrtrcl5  37936  iunrelexp0  37994  relexpmulg  38002  relexp01min  38005  relexpxpmin  38009  brtrclfv2  38019  sge0resplit  40623  sge0split  40626  setsv  41348  setrec1lem4  42437