Theorem unisn 4885

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

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2144  Vcvv 3450  {csn 4584  ∪ cuni 4866

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3897  df-un 4150  df-sn 4585  df-pr 4587  df-uni 4867

This theorem is used by:  unisnv  4886  unidif0  5320  unidif0OLD  5321  op1sta  6228  op2nda  6231  opswap  6232  funfv  6975  dffv2  6983  nlim1  8502  tc2  9746  fin1a2lem12  10494  acsmapd  18735  ghmqusnsglem1  19501  ghmquskerlem1  19504  pmtrprfval  19708  lspuni0  21292  lss0v  21298  zrhval2  21821  indistopon  23326  refun0  23841  qtopeu  24042  hmphindis  24123  filconn  24209  ufildr  24257  cnextfres1  24394  bday1  28207  old1  28258  madeoldsuc  28278  dimval  34281  dimvalfi  34282  locfinref  34521  pstmfval  34576  esumval  34726  esumpfinval  34755  esumpfinvalf  34756  prsiga  34811  carsggect  34998  fineqvnttrclse  35850  indispconn  36087  onsucsuccmpi  37325  bj-nuliotaALT  38079  heiborlem3  38854  isomenndlem  47647  uniimaelsetpreimafv  48585