Theorem unex 4538

Description: The union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 1-Jul-1994.)

Hypotheses

Ref	Expression
unex.1	|- A e. _V
unex.2	|- B e. _V

Assertion

Ref	Expression
unex	|- ( A u. B ) e. _V

Proof of Theorem unex

Step	Hyp	Ref	Expression
1		unex.1	. . 3 |- A e. _V
2		unex.2	. . 3 |- B e. _V
3	1, 2	unipr 3907	. 2 |- U. { A , B } = ( A u. B )
4		prexg 4301	. . . 4 |- ( ( A e. _V /\ B e. _V ) -> { A , B } e. _V )
5	1, 2, 4	mp2an 426	. . 3 |- { A , B } e. _V
6	5	uniex 4534	. 2 |- U. { A , B } e. _V
7	3, 6	eqeltrri 2305	1 |- ( A u. B ) e. _V

Syntax hints:   e. wcel 2202   _Vcvv 2802   u. cun 3198   {cpr 3670   U.cuni 3893

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pr 4299  ax-un 4530

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-uni 3894

This theorem is referenced by:  unexb  4539  rdg0  6552  unen  6990  findcard2  7077  findcard2s  7078  ac6sfi  7086  sbthlemi10  7164  finomni  7338  exmidfodomrlemim  7411  nn0ex  9407  xrex  10090  xnn0nnen  10698  nninfct  12611  exmidunben  13046  strleun  13186  fngsum  13470  fnpsr  14680