Theorem unisn 4260

Description: A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 30-Aug-1993.)

Hypothesis

Ref	Expression
unisn.1	|- A e. _V

Assertion

Ref	Expression
unisn	|- U. { A } = A

Proof of Theorem unisn

Step	Hyp	Ref	Expression
1		dfsn2 4040	. . 3 |- { A } = { A , A }
2	1	unieqi 4254	. 2 |- U. { A } = U. { A , A }
3		unisn.1	. . 3 |- A e. _V
4	3, 3	unipr 4258	. 2 |- U. { A , A } = ( A u. A )
5		unidm 3647	. 2 |- ( A u. A ) = A
6	2, 4, 5	3eqtri 2500	1 |- U. { A } = A

Syntax hints:   = wceq 1379   e. wcel 1767   _Vcvv 3113   u. cun 3474   {csn 4027   {cpr 4029   U.cuni 4245

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820  df-v 3115  df-un 3481  df-sn 4028  df-pr 4030  df-uni 4246

This theorem is referenced by:  unisng  4261  uniintsn  4319  unidif0  4620  unisuc  4954  op1sta  5488  op2nda  5491  opswap  5493  uniabio  5559  fvssunirn  5887  opabiotafun  5926  funfv  5932  dffv2  5938  onuninsuci  6653  en1b  7580  tc2  8169  cflim2  8639  fin1a2lem10  8785  fin1a2lem12  8787  incexclem  13604  acsmapd  15658  pmtrprfval  16305  sylow2a  16432  lspuni0  17436  lss0v  17442  zrhval2  18310  indistopon  19265  1stckgenlem  19786  qtopeu  19949  hmphindis  20030  filcon  20116  ufildr  20164  alexsubALTlem3  20281  ptcmplem2  20285  cnextfres  20300  icccmplem1  21059  disjabrex  27113  disjabrexf  27114  pstmfval  27508  esumval  27694  esumpfinval  27718  esumpfinvalf  27719  prsiga  27768  indispcon  28316  fobigcup  29124  onsucsuccmpi  29482  mbfresfi  29636  heiborlem3  29910  bj-nuliotaALT  33668