Theorem unisn 4864

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

Syntax hints:   = wceq 1547   ∈ wcel 2119  Vcvv 3432  {csn 4562  ∪ cuni 4845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-ss 3907  df-sn 4563  df-pr 4565  df-uni 4846

This theorem is referenced by:  unisnv  4865  unidif0  5295  unidif0OLD  5296  op1sta  6183  op2nda  6186  opswap  6187  funfv  6921  dffv2  6929  nlim1  8421  tc2  9659  cflim2  10183  fin1a2lem12  10331  acsmapd  18518  ghmqusnsglem1  19253  ghmquskerlem1  19256  pmtrprfval  19460  lspuni0  21007  lss0v  21013  zrhval2  21490  indistopon  22991  refun0  23505  qtopeu  23706  hmphindis  23787  filconn  23873  ufildr  23921  cnextfres1  24058  bday1  27831  old1  27882  madeoldsuc  27902  dimval  33792  dimvalfi  33793  locfinref  34032  pstmfval  34087  esumval  34237  esumpfinval  34266  esumpfinvalf  34267  prsiga  34322  carsggect  34509  fineqvnttrclse  35312  indispconn  35469  onsucsuccmpi  36678  bj-nuliotaALT  37418  heiborlem3  38187  isomenndlem  46980  uniimaelsetpreimafv  47878