Theorem unisn 4208

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 3987	. . 3 |- { A } = { A , A }
2	1	unieqi 4202	. 2 |- U. { A } = U. { A , A }
3		unisn.1	. . 3 |- A e. _V
4	3, 3	unipr 4206	. 2 |- U. { A , A } = ( A u. A )
5		unidm 3588	. 2 |- ( A u. A ) = A
6	2, 4, 5	3eqtri 2437	1 |- U. { A } = A

Syntax hints:   = wceq 1407   e. wcel 1844   _Vcvv 3061   u. cun 3414   {csn 3974   {cpr 3976   U.cuni 4193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382

This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-rex 2762  df-v 3063  df-un 3421  df-sn 3975  df-pr 3977  df-uni 4194

This theorem is referenced by:  unisng  4209  uniintsn  4267  unidif0  4569  op1sta  5308  op2nda  5311  opswap  5313  unisuc  5488  uniabio  5545  fvssunirn  5874  opabiotafun  5912  funfv  5918  dffv2  5924  onuninsuci  6660  en1b  7623  tc2  8207  cflim2  8677  fin1a2lem10  8823  fin1a2lem12  8825  incexclem  13801  acsmapd  16134  pmtrprfval  16838  sylow2a  16965  lspuni0  17978  lss0v  17984  zrhval2  18848  indistopon  19796  refun0  20310  1stckgenlem  20348  qtopeu  20511  hmphindis  20592  filcon  20678  ufildr  20726  alexsubALTlem3  20843  ptcmplem2  20847  cnextfres  20862  icccmplem1  21621  disjabrex  27887  disjabrexf  27888  locfinref  28310  pstmfval  28341  esumval  28506  esumpfinval  28535  esumpfinvalf  28536  prsiga  28592  fiunelcarsg  28777  carsgclctunlem1  28778  carsggect  28779  indispcon  29544  fobigcup  30251  onsucsuccmpi  30688  bj-nuliotaALT  31165  mbfresfi  31446  heiborlem3  31604