Theorem unisn 4870

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  Vcvv 3430  {csn 4568  ∪ cuni 4851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-ss 3907  df-sn 4569  df-pr 4571  df-uni 4852

This theorem is referenced by:  unisnv  4871  unidif0  5297  op1sta  6183  op2nda  6186  opswap  6187  funfv  6921  dffv2  6929  nlim1  8417  tc2  9652  cflim2  10176  fin1a2lem12  10324  acsmapd  18511  ghmqusnsglem1  19246  ghmquskerlem1  19249  pmtrprfval  19453  lspuni0  20996  lss0v  21003  zrhval2  21498  indistopon  22976  refun0  23490  qtopeu  23691  hmphindis  23772  filconn  23858  ufildr  23906  cnextfres1  24043  bday1  27820  old1  27871  madeoldsuc  27891  dimval  33760  dimvalfi  33761  locfinref  34001  pstmfval  34056  esumval  34206  esumpfinval  34235  esumpfinvalf  34236  prsiga  34291  carsggect  34478  fineqvnttrclse  35284  indispconn  35432  onsucsuccmpi  36641  bj-nuliotaALT  37381  heiborlem3  38148  isomenndlem  46976  uniimaelsetpreimafv  47868