Theorem unisn 4264

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

Assertion

Ref	Expression
unisn

Proof of Theorem unisn

Step	Hyp	Ref	Expression
1		dfsn2 4042	. . 3
2	1	unieqi 4258	. 2
3		unisn.1	. . 3
4	3, 3	unipr 4262	. 2
5		unidm 3646	. 2
6	2, 4, 5	3eqtri 2490	1

Syntax hints:  =wceq 1395  e.wcel 1818  cvv 3109  u.cun 3473  {csn 4029  {cpr 4031  U.cuni 4249

This theorem is referenced by:  unisng  4265  uniintsn  4324  unidif0  4625  unisuc  4959  op1sta  5495  op2nda  5498  opswap  5500  uniabio  5566  fvssunirn  5894  opabiotafun  5934  funfv  5940  dffv2  5946  onuninsuci  6675  en1b  7603  tc2  8194  cflim2  8664  fin1a2lem10  8810  fin1a2lem12  8812  incexclem  13648  acsmapd  15808  pmtrprfval  16512  sylow2a  16639  lspuni0  17656  lss0v  17662  zrhval2  18546  indistopon  19502  refun0  20016  1stckgenlem  20054  qtopeu  20217  hmphindis  20298  filcon  20384  ufildr  20432  alexsubALTlem3  20549  ptcmplem2  20553  cnextfres  20568  icccmplem1  21327  disjabrex  27443  disjabrexf  27444  locfinref  27844  pstmfval  27875  esumval  28057  esumpfinval  28081  esumpfinvalf  28082  prsiga  28131  indispcon  28679  fobigcup  29550  onsucsuccmpi  29908  mbfresfi  30061  heiborlem3  30309  bj-nuliotaALT  34587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-v 3111  df-un 3480  df-sn 4030  df-pr 4032  df-uni 4250