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 4583  ∪ 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 3896  df-un 4151  df-sn 4584  df-pr 4586  df-uni 4867

This theorem is used by:  unisnv  4886  unidif0  5320  unidif0OLD  5321  op1sta  6226  op2nda  6229  opswap  6230  funfv  6972  dffv2  6980  nlim1  8498  tc2  9742  cflim2  10342  fin1a2lem12  10490  acsmapd  18729  ghmqusnsglem1  19495  ghmquskerlem1  19498  pmtrprfval  19702  lspuni0  21286  lss0v  21292  zrhval2  21815  indistopon  23320  refun0  23835  qtopeu  24036  hmphindis  24117  filconn  24203  ufildr  24251  cnextfres1  24388  bday1  28201  old1  28252  madeoldsuc  28272  dimval  34276  dimvalfi  34277  locfinref  34516  pstmfval  34571  esumval  34721  esumpfinval  34750  esumpfinvalf  34751  prsiga  34806  carsggect  34993  fineqvnttrclse  35841  indispconn  36068  onsucsuccmpi  37306  bj-nuliotaALT  38048  heiborlem3  38823  isomenndlem  47616  uniimaelsetpreimafv  48554