Theorem unisn 2514

Description: A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53.

Hypothesis

Ref	Expression
unisn.1	|- A e. V

Assertion

Ref	Expression
unisn	|- U.{A} = A

Proof of Theorem unisn

Step	Hyp	Ref	Expression
1		dfsn2 2418	. . 3 |- {A} = {A, A}
2	1	unieqi 2508	. 2 |- U.{A} = U.{A, A}
3		unisn.1	. . 3 |- A e. V
4	3, 3	unipr 2512	. 2 |- U.{A, A} = (A u. A)
5		unidm 2173	. 2 |- (A u. A) = A
6	2, 4, 5	3eqtr 1498	1 |- U.{A} = A

Syntax hints:   = wceq 955   e. wcel 957  Vcvv 1809   u. cun 2043  {csn 2407  {cpr 2408  U.cuni 2500

This theorem is referenced by:  unisng 2515  unidif0 2736  euuni 2878  reucl 2882  rabsnt 2891  reuunisn 2892  unisuc 3043  onuninsuc 3105  op1sta 3445  unixp0 3515  fvex 3729  funfv 3767  ecqs 4294  xpcomen 4432  unifi 4545  subtop 7625  sn0top 7626  indistop 7627

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1810  df-un 2048  df-sn 2410  df-pr 2411  df-uni 2501

Copyright terms: Public domain