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 3450  {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 2732

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-ss 3916  df-sn 4585  df-pr 4587  df-uni 4868

This theorem is used by:  unisnv  4887  unidif0  5324  unidif0OLD  5325  op1sta  6221  op2nda  6224  opswap  6225  funfv  6965  dffv2  6973  nlim1  8476  tc2  9719  cflim2  10265  fin1a2lem12  10413  acsmapd  18642  ghmqusnsglem1  19407  ghmquskerlem1  19410  pmtrprfval  19614  lspuni0  21194  lss0v  21200  zrhval2  21721  indistopon  23226  refun0  23741  qtopeu  23942  hmphindis  24023  filconn  24109  ufildr  24157  cnextfres1  24294  bday1  28079  old1  28130  madeoldsuc  28150  dimval  34111  dimvalfi  34112  locfinref  34351  pstmfval  34406  esumval  34556  esumpfinval  34585  esumpfinvalf  34586  prsiga  34641  carsggect  34829  fineqvnttrclse  35650  indispconn  35813  onsucsuccmpi  37062  bj-nuliotaALT  37802  heiborlem3  38563  isomenndlem  47358  uniimaelsetpreimafv  48296