Theorem unisn 2531

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 2432	. . 3 |- {A} = {A, A}
2	1	unieqi 2525	. 2 |- U.{A} = U.{A, A}
3		unisn.1	. . 3 |- A e. V
4	3, 3	unipr 2529	. 2 |- U.{A, A} = (A u. A)
5		unidm 2186	. 2 |- (A u. A) = A
6	2, 4, 5	3eqtri 1506	1 |- U.{A} = A

Syntax hints:   = wceq 960   e. wcel 962  Vcvv 1818   u. cun 2056  {csn 2421  {cpr 2422  U.cuni 2517

This theorem is referenced by:  unisng 2532  unidif0 2754  euuni 2897  reucl 2901  rabsnt 2910  reuunisn 2911  unisuc 3062  onuninsuci 3124  op1sta 3464  unixp0 3534  fvex 3748  funfv 3786  ecqs 4315  fiprlem 4451  xpcomen 4458  unifi 4573  subtop 7674  sn0top 7675  indistop 7676

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-10 970  ax-12 972  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1127  ax-10o 1144  ax-16 1214  ax-11o 1222  ax-ext 1464

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 985  df-sb 1176  df-clab 1470  df-cleq 1475  df-clel 1478  df-v 1819  df-un 2061  df-sn 2424  df-pr 2425  df-uni 2518

Copyright terms: Public domain