Theorem unisn 4600

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		dfsn2 4339	. . 3 ⊢ {𝐴} = {𝐴, 𝐴}
2	1	unieqi 4594	. 2 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴}
3		unisn.1	. . 3 ⊢ 𝐴 ∈ V
4	3, 3	unipr 4598	. 2 ⊢ ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴)
5		unidm 3914	. 2 ⊢ (𝐴 ∪ 𝐴) = 𝐴
6	2, 4, 5	3eqtri 2800	1 ⊢ ∪ {𝐴} = 𝐴

Syntax hints:   = wceq 1634   ∈ wcel 2148  Vcvv 3355   ∪ cun 3727  {csn 4326  {cpr 4328  ∪ cuni 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754

This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-rex 3070  df-v 3357  df-un 3734  df-sn 4327  df-pr 4329  df-uni 4586

This theorem is referenced by:  unisng  4601  uniintsn  4659  unidif0  4983  op1sta  5771  op2nda  5775  opswap  5777  unisuc  5955  uniabio  6015  fvssunirn  6375  opabiotafun  6418  funfv  6424  dffv2  6430  onuninsuci  7208  en1b  8198  tc2  8803  cflim2  9308  fin1a2lem10  9454  fin1a2lem12  9456  incexclem  14797  acsmapd  17406  pmtrprfval  18134  sylow2a  18261  lspuni0  19243  lss0v  19249  zrhval2  20092  indistopon  21046  refun0  21559  1stckgenlem  21597  qtopeu  21760  hmphindis  21841  filconn  21927  ufildr  21975  alexsubALTlem3  22093  ptcmplem2  22097  cnextfres1  22112  icccmplem1  22865  disjabrex  29750  disjabrexf  29751  locfinref  30265  pstmfval  30296  esumval  30465  esumpfinval  30494  esumpfinvalf  30495  prsiga  30551  fiunelcarsg  30735  carsgclctunlem1  30736  carsggect  30737  indispconn  31571  fobigcup  32361  onsucsuccmpi  32796  bj-nuliotaALT  33368  mbfresfi  33805  heiborlem3  33960  prsal  41061  isomenndlem  41270