Theorem unexg 4564

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	|- ( ( A e. V /\ B e. W ) -> ( A u. B ) e. _V )

Proof of Theorem unexg

Step	Hyp	Ref	Expression
1		elex 2825	. 2 |- ( A e. V -> A e. _V )
2		elex 2825	. 2 |- ( B e. W -> B e. _V )
3		unexb 4563	. . 3 |- ( ( A e. _V /\ B e. _V ) <-> ( A u. B ) e. _V )
4	3	biimpi 120	. 2 |- ( ( A e. _V /\ B e. _V ) -> ( A u. B ) e. _V )
5	1, 2, 4	syl2an 289	1 |- ( ( A e. V /\ B e. W ) -> ( A u. B ) e. _V )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2203   _Vcvv 2813   u. cun 3209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pr 4322  ax-un 4554

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-v 2815  df-un 3215  df-in 3217  df-ss 3224  df-sn 3695  df-pr 3696  df-uni 3915

This theorem is referenced by:  tpexg  4565  eldifpw  4598  ifelpwung  4602  xpexg  4864  unexd  4867  tposexg  6489  tfrlemisucaccv  6556  tfrlemibxssdm  6558  tfrlemibfn  6559  tfr1onlemsucaccv  6572  tfr1onlembxssdm  6574  tfr1onlembfn  6575  tfrcllemsucaccv  6585  tfrcllembxssdm  6587  tfrcllembfn  6588  rdgtfr  6605  rdgruledefgg  6606  rdgivallem  6612  djuex  7334  hashfibclem  11206  zfz1isolem1  11212  ennnfonelemp1  13157  setsvalg  13242  setsex  13244  setsslid  13263  strleund  13316  prdsex  13482  prdsval  13486  igsumvalx  13602  psrval  14814  plyval  15597  elply2  15600  plyss  15603  plyco  15624  plycj  15626  uhgrunop  16082  upgrunop  16122  umgrunop  16124