Theorem unex 2872

Description: The union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16.

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 2515	. 2 |- U.{A, B} = (A u. B)
4		prex 2781	. . 3 |- {A, B} e. V
5	4	uniex 2870	. 2 |- U.{A, B} e. V
6	3, 5	eqeltrr 1545	1 |- (A u. B) e. V

Syntax hints:   e. wcel 958  Vcvv 1811   u. cun 2045  {cpr 2410  U.cuni 2503

This theorem is referenced by:  unexb 2873  tpex 2878  fvclex 3856  unen 4434  undom 4438  mapunen 4502  abfii4OLD 4564  pwfilemOLD 4570  trcl 4645  rankun 4691  rankelun 4707  rankxpu 4711  rankxplim 4712  rankxplim3 4714  kmlem2 4766  unxpdomlem 4843  cdaassen 4930  xpcdaen 4931  xrex 5492  sumex 6981  acdc2lem2 7489  acdc5lem2 7492  ruclem5 7514  infxpidmlem9 7560  infxpidmlem11 7562  infxpidmlem12 7563  infdif 7568  subbasOLD 7644  infi1 10447  infi1OLD 10448  ficli 10472  ficliOLD 10473  infi 10578  infiOLD 10579  rcfpfillem4 10591  rcfpfillem4OLD 10592

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-pow 2742  ax-pr 2779  ax-un 2866

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-uni 2504

Copyright terms: Public domain