Theorem unisn 4931

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

Syntax hints:   = wceq 1537   ∈ wcel 2106  Vcvv 3478  {csn 4631  ∪ cuni 4912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-ss 3980  df-sn 4632  df-pr 4634  df-uni 4913

This theorem is referenced by:  unisnv  4932  unidif0  5366  op1sta  6247  op2nda  6250  opswap  6251  fvssunirnOLD  6941  funfv  6996  dffv2  7004  nlim1  8526  tc2  9780  cflim2  10301  fin1a2lem12  10449  acsmapd  18612  ghmqusnsglem1  19311  ghmquskerlem1  19314  pmtrprfval  19520  lspuni0  21026  lss0v  21033  zrhval2  21537  indistopon  23024  refun0  23539  qtopeu  23740  hmphindis  23821  filconn  23907  ufildr  23955  cnextfres1  24092  bday1s  27891  old1  27929  madeoldsuc  27938  zs12bday  28439  dimval  33628  dimvalfi  33629  locfinref  33802  pstmfval  33857  esumval  34027  esumpfinval  34056  esumpfinvalf  34057  prsiga  34112  carsggect  34300  indispconn  35219  onsucsuccmpi  36426  bj-nuliotaALT  37041  heiborlem3  37800  isomenndlem  46486  uniimaelsetpreimafv  47321