Theorem unisn 4249

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 4027	. . 3 |- { A } = { A , A }
2	1	unieqi 4243	. 2 |- U. { A } = U. { A , A }
3		unisn.1	. . 3 |- A e. _V
4	3, 3	unipr 4247	. 2 |- U. { A , A } = ( A u. A )
5		unidm 3632	. 2 |- ( A u. A ) = A
6	2, 4, 5	3eqtri 2476	1 |- U. { A } = A

Syntax hints:   = wceq 1383   e. wcel 1804   _Vcvv 3095   u. cun 3459   {csn 4014   {cpr 4016   U.cuni 4234

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rex 2799  df-v 3097  df-un 3466  df-sn 4015  df-pr 4017  df-uni 4235

This theorem is referenced by:  unisng  4250  uniintsn  4309  unidif0  4610  unisuc  4944  op1sta  5480  op2nda  5483  opswap  5485  uniabio  5551  fvssunirn  5879  opabiotafun  5919  funfv  5925  dffv2  5931  onuninsuci  6660  en1b  7585  tc2  8176  cflim2  8646  fin1a2lem10  8792  fin1a2lem12  8794  incexclem  13630  acsmapd  15787  pmtrprfval  16491  sylow2a  16618  lspuni0  17635  lss0v  17641  zrhval2  18524  indistopon  19480  refun0  19994  1stckgenlem  20032  qtopeu  20195  hmphindis  20276  filcon  20362  ufildr  20410  alexsubALTlem3  20527  ptcmplem2  20531  cnextfres  20546  icccmplem1  21305  disjabrex  27421  disjabrexf  27422  locfinref  27822  pstmfval  27853  esumval  28035  esumpfinval  28059  esumpfinvalf  28060  prsiga  28109  indispcon  28657  fobigcup  29526  onsucsuccmpi  29884  mbfresfi  30037  heiborlem3  30285  bj-nuliotaALT  34470