Theorem unisn 4892

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

Syntax hints:   = wceq 1567   ∈ wcel 2149  Vcvv 3463  {csn 4591  ∪ cuni 4873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-ss 3930  df-sn 4592  df-pr 4594  df-uni 4874

This theorem is referenced by:  unisnv  4893  unidif0  5328  unidif0OLD  5329  op1sta  6223  op2nda  6226  opswap  6227  funfv  6966  dffv2  6974  nlim1  8470  tc2  9705  cflim2  10243  fin1a2lem12  10391  acsmapd  18606  ghmqusnsglem1  19346  ghmquskerlem1  19349  pmtrprfval  19553  lspuni0  21105  lss0v  21111  zrhval2  21623  indistopon  23123  refun0  23637  qtopeu  23838  hmphindis  23919  filconn  24005  ufildr  24053  cnextfres1  24190  bday1  27969  old1  28020  madeoldsuc  28040  dimval  33932  dimvalfi  33933  locfinref  34172  pstmfval  34227  esumval  34377  esumpfinval  34406  esumpfinvalf  34407  prsiga  34462  carsggect  34649  fineqvnttrclse  35456  indispconn  35621  onsucsuccmpi  36839  bj-nuliotaALT  37578  heiborlem3  38347  isomenndlem  47129  uniimaelsetpreimafv  48027