Theorem unisn 4451

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	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
unisn	⊢ ∪ {𝐴} = 𝐴

Proof of Theorem unisn

Step	Hyp	Ref	Expression
1		dfsn2 4190	. . 3 ⊢ {𝐴} = {𝐴, 𝐴}
2	1	unieqi 4445	. 2 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴}
3		unisn.1	. . 3 ⊢ 𝐴 ∈ V
4	3, 3	unipr 4449	. 2 ⊢ ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴)
5		unidm 3756	. 2 ⊢ (𝐴 ∪ 𝐴) = 𝐴
6	2, 4, 5	3eqtri 2648	1 ⊢ ∪ {𝐴} = 𝐴

Syntax hints:   = wceq 1483   ∈ wcel 1990  Vcvv 3200   ∪ cun 3572  {csn 4177  {cpr 4179  ∪ cuni 4436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-v 3202  df-un 3579  df-sn 4178  df-pr 4180  df-uni 4437

This theorem is referenced by:  unisng  4452  uniintsn  4514  unidif0  4838  op1sta  5617  op2nda  5620  opswap  5622  unisuc  5801  uniabio  5861  fvssunirn  6217  opabiotafun  6259  funfv  6265  dffv2  6271  onuninsuci  7040  en1b  8024  tc2  8618  cflim2  9085  fin1a2lem10  9231  fin1a2lem12  9233  incexclem  14568  acsmapd  17178  pmtrprfval  17907  sylow2a  18034  lspuni0  19010  lss0v  19016  zrhval2  19857  indistopon  20805  refun0  21318  1stckgenlem  21356  qtopeu  21519  hmphindis  21600  filconn  21687  ufildr  21735  alexsubALTlem3  21853  ptcmplem2  21857  cnextfres1  21872  icccmplem1  22625  disjabrex  29395  disjabrexf  29396  locfinref  29908  pstmfval  29939  esumval  30108  esumpfinval  30137  esumpfinvalf  30138  prsiga  30194  fiunelcarsg  30378  carsgclctunlem1  30379  carsggect  30380  indispconn  31216  fobigcup  32007  onsucsuccmpi  32442  bj-nuliotaALT  33020  mbfresfi  33456  heiborlem3  33612  prsal  40538  isomenndlem  40744