Theorem unisn 4886

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  Vcvv 3451  {csn 4584  ∪ cuni 4867

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916  df-sn 4585  df-pr 4587  df-uni 4868

This theorem is used by:  unisnv  4887  unidif0  5321  unidif0OLD  5322  op1sta  6225  op2nda  6228  opswap  6229  funfv  6970  dffv2  6978  nlim1  8490  tc2  9734  cflim2  10334  fin1a2lem12  10482  acsmapd  18721  ghmqusnsglem1  19487  ghmquskerlem1  19490  pmtrprfval  19694  lspuni0  21278  lss0v  21284  zrhval2  21807  indistopon  23312  refun0  23827  qtopeu  24028  hmphindis  24109  filconn  24195  ufildr  24243  cnextfres1  24380  bday1  28193  old1  28244  madeoldsuc  28264  dimval  34226  dimvalfi  34227  locfinref  34466  pstmfval  34521  esumval  34671  esumpfinval  34700  esumpfinvalf  34701  prsiga  34756  carsggect  34943  fineqvnttrclse  35775  indispconn  35978  onsucsuccmpi  37211  bj-nuliotaALT  37953  heiborlem3  38727  isomenndlem  47509  uniimaelsetpreimafv  48447