Theorem unisn 4761

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		unisn.1	. 2 ⊢ 𝐴 ∈ V
2		unisng 4760	. 2 ⊢ (𝐴 ∈ V → ∪ {𝐴} = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ ∪ {𝐴} = 𝐴

Syntax hints:   = wceq 1522   ∈ wcel 2081  Vcvv 3437  {csn 4472  ∪ cuni 4745

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-rex 3111  df-v 3439  df-un 3864  df-sn 4473  df-pr 4475  df-uni 4746

This theorem is referenced by:  uniintsn  4819  unidif0  5151  op1sta  5957  op2nda  5960  opswap  5961  unisuc  6142  uniabio  6199  fvssunirn  6567  opabiotafun  6611  funfv  6617  dffv2  6623  onuninsuci  7411  en1b  8425  tc2  9030  cflim2  9531  fin1a2lem10  9677  fin1a2lem12  9679  incexclem  15024  acsmapd  17617  pmtrprfval  18346  sylow2a  18474  lspuni0  19472  lss0v  19478  zrhval2  20338  indistopon  21293  refun0  21807  1stckgenlem  21845  qtopeu  22008  hmphindis  22089  filconn  22175  ufildr  22223  alexsubALTlem3  22341  ptcmplem2  22345  cnextfres1  22360  icccmplem1  23113  unidifsnel  29984  unidifsnne  29985  disjabrex  30022  disjabrexf  30023  dimval  30605  dimvalfi  30606  locfinref  30722  pstmfval  30753  esumval  30922  esumpfinval  30951  esumpfinvalf  30952  prsiga  31007  fiunelcarsg  31191  carsgclctunlem1  31192  carsggect  31193  indispconn  32089  fobigcup  32970  onsucsuccmpi  33400  bj-nuliotaALT  33949  mbfresfi  34469  heiborlem3  34623  isomenndlem  42354