Theorem unisn 4227

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 3993	. . 3 |- { A } = { A , A }
2	1	unieqi 4221	. 2 |- U. { A } = U. { A , A }
3		unisn.1	. . 3 |- A e. _V
4	3, 3	unipr 4225	. 2 |- U. { A , A } = ( A u. A )
5		unidm 3589	. 2 |- ( A u. A ) = A
6	2, 4, 5	3eqtri 2488	1 |- U. { A } = A

Syntax hints:   = wceq 1455   e. wcel 1898   _Vcvv 3057   u. cun 3414   {csn 3980   {cpr 3982   U.cuni 4212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rex 2755  df-v 3059  df-un 3421  df-sn 3981  df-pr 3983  df-uni 4213

This theorem is referenced by:  unisng  4228  uniintsn  4286  unidif0  4593  op1sta  5341  op2nda  5344  opswap  5346  unisuc  5522  uniabio  5579  fvssunirn  5915  opabiotafun  5954  funfv  5960  dffv2  5966  onuninsuci  6699  en1b  7668  tc2  8257  cflim2  8724  fin1a2lem10  8870  fin1a2lem12  8872  incexclem  13949  acsmapd  16479  pmtrprfval  17183  sylow2a  17326  lspuni0  18288  lss0v  18294  zrhval2  19135  indistopon  20071  refun0  20585  1stckgenlem  20623  qtopeu  20786  hmphindis  20867  filcon  20953  ufildr  21001  alexsubALTlem3  21119  ptcmplem2  21123  cnextfres1  21138  icccmplem1  21895  disjabrex  28246  disjabrexf  28247  locfinref  28719  pstmfval  28750  esumval  28918  esumpfinval  28947  esumpfinvalf  28948  prsiga  29004  fiunelcarsg  29198  carsgclctunlem1  29199  carsggect  29200  indispcon  30007  fobigcup  30717  onsucsuccmpi  31153  bj-nuliotaALT  31670  mbfresfi  32033  heiborlem3  32191  prsal  38280  isomenndlem  38459