Theorem unisn 4902

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  Vcvv 3459  {csn 4601  ∪ cuni 4883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-ss 3943  df-sn 4602  df-pr 4604  df-uni 4884

This theorem is referenced by:  unisnv  4903  unidif0  5330  op1sta  6214  op2nda  6217  opswap  6218  fvssunirnOLD  6910  funfv  6966  dffv2  6974  nlim1  8501  tc2  9756  cflim2  10277  fin1a2lem12  10425  acsmapd  18564  ghmqusnsglem1  19263  ghmquskerlem1  19266  pmtrprfval  19468  lspuni0  20967  lss0v  20974  zrhval2  21469  indistopon  22939  refun0  23453  qtopeu  23654  hmphindis  23735  filconn  23821  ufildr  23869  cnextfres1  24006  bday1s  27795  old1  27839  madeoldsuc  27848  zs12bday  28395  dimval  33640  dimvalfi  33641  locfinref  33872  pstmfval  33927  esumval  34077  esumpfinval  34106  esumpfinvalf  34107  prsiga  34162  carsggect  34350  indispconn  35256  onsucsuccmpi  36461  bj-nuliotaALT  37076  heiborlem3  37837  isomenndlem  46559  uniimaelsetpreimafv  47410