Theorem unisn 4106

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 3890	. . 3 |- { A } = { A , A }
2	1	unieqi 4100	. 2 |- U. { A } = U. { A , A }
3		unisn.1	. . 3 |- A e. _V
4	3, 3	unipr 4104	. 2 |- U. { A , A } = ( A u. A )
5		unidm 3499	. 2 |- ( A u. A ) = A
6	2, 4, 5	3eqtri 2467	1 |- U. { A } = A

Syntax hints:   = wceq 1369   e. wcel 1756   _Vcvv 2972   u. cun 3326   {csn 3877   {cpr 3879   U.cuni 4091

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-rex 2721  df-v 2974  df-un 3333  df-sn 3878  df-pr 3880  df-uni 4092

This theorem is referenced by:  unisng  4107  uniintsn  4165  unidif0  4465  unisuc  4795  op1sta  5321  op2nda  5324  opswap  5326  uniabio  5391  fvssunirn  5713  opabiotafun  5752  funfv  5758  dffv2  5764  onuninsuci  6451  en1b  7377  tc2  7962  cflim2  8432  fin1a2lem10  8578  fin1a2lem12  8580  incexclem  13299  acsmapd  15348  pmtrprfval  15993  sylow2a  16118  lspuni0  17091  lss0v  17097  zrhval2  17940  indistopon  18605  1stckgenlem  19126  qtopeu  19289  hmphindis  19370  filcon  19456  ufildr  19504  alexsubALTlem3  19621  ptcmplem2  19625  cnextfres  19640  icccmplem1  20399  disjabrex  25926  disjabrexf  25927  pstmfval  26323  esumval  26500  esumpfinval  26524  esumpfinvalf  26525  prsiga  26574  indispcon  27123  fobigcup  27931  onsucsuccmpi  28289  mbfresfi  28438  heiborlem3  28712