Theorem unisn 4934

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

Syntax hints:   = wceq 1534   ∈ wcel 2099  Vcvv 3462  {csn 4633  ∪ cuni 4913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-un 3952  df-ss 3964  df-sn 4634  df-pr 4636  df-uni 4914

This theorem is referenced by:  unisnv  4935  unidif0  5364  op1sta  6236  op2nda  6239  opswap  6240  fvssunirnOLD  6935  funfv  6989  dffv2  6997  nlim1  8519  en1bOLD  9060  tc2  9785  cflim2  10306  fin1a2lem12  10454  acsmapd  18579  ghmqusnsglem1  19274  ghmquskerlem1  19277  pmtrprfval  19485  lspuni0  20987  lss0v  20994  zrhval2  21498  indistopon  22995  refun0  23510  qtopeu  23711  hmphindis  23792  filconn  23878  ufildr  23926  cnextfres1  24063  bday1s  27861  old1  27899  madeoldsuc  27908  dimval  33495  dimvalfi  33496  locfinref  33656  pstmfval  33711  esumval  33879  esumpfinval  33908  esumpfinvalf  33909  prsiga  33964  carsggect  34152  indispconn  35062  onsucsuccmpi  36155  bj-nuliotaALT  36765  heiborlem3  37514  isomenndlem  46151  uniimaelsetpreimafv  46968