Theorem unisng 2585

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

Assertion

Ref	Expression
unisng	⊢ (A ∈ B → ∪{A} = A)

Proof of Theorem unisng

Step	Hyp	Ref	Expression
1		sneq 2475	. . . 4 ⊢ (x = A → {x} = {A})
2	1	unieqd 2578	. . 3 ⊢ (x = A → ∪{x} = ∪{A})
3		id 59	. . 3 ⊢ (x = A → x = A)
4	2, 3	eqeq12d 1532	. 2 ⊢ (x = A → (∪{x} = x ↔ ∪{A} = A))
5		visset 1859	. . 3 ⊢ x ∈ V
6	5	unisn 2583	. 2 ⊢ ∪{x} = x
7	4, 6	vtoclg 1893	1 ⊢ (A ∈ B → ∪{A} = A)

Syntax hints:   → wi 3   = wceq 992   ∈ wcel 994  {csn 2467  ∪cuni 2569

This theorem is referenced by:  unisn2 3098  unisn3 3099  fvopab6 3905  indistop 7860  chsupsn 9588  oefil2 11079  cptclsscpt 11489  fnejoin2 11592  extbas2 11642  ufileu 11658  filufint 11659  uffixfr 11660  flimcls 11684

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-un 2102  df-sn 2470  df-pr 2471  df-uni 2570

Copyright terms: Public domain