Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  unisn Structured version   Visualization version   GIF version

Theorem unisn 4483
 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
StepHypRef Expression
1 dfsn2 4223 . . 3 {𝐴} = {𝐴, 𝐴}
21unieqi 4477 . 2 {𝐴} = {𝐴, 𝐴}
3 unisn.1 . . 3 𝐴 ∈ V
43, 3unipr 4481 . 2 {𝐴, 𝐴} = (𝐴𝐴)
5 unidm 3789 . 2 (𝐴𝐴) = 𝐴
62, 4, 53eqtri 2677 1 {𝐴} = 𝐴
 Colors of variables: wff setvar class Syntax hints:   = wceq 1523   ∈ wcel 2030  Vcvv 3231   ∪ cun 3605  {csn 4210  {cpr 4212  ∪ cuni 4468 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-v 3233  df-un 3612  df-sn 4211  df-pr 4213  df-uni 4469 This theorem is referenced by:  unisng  4484  uniintsn  4546  unidif0  4868  op1sta  5654  op2nda  5658  opswap  5660  unisuc  5839  uniabio  5899  fvssunirn  6255  opabiotafun  6298  funfv  6304  dffv2  6310  onuninsuci  7082  en1b  8065  tc2  8656  cflim2  9123  fin1a2lem10  9269  fin1a2lem12  9271  incexclem  14612  acsmapd  17225  pmtrprfval  17953  sylow2a  18080  lspuni0  19058  lss0v  19064  zrhval2  19905  indistopon  20853  refun0  21366  1stckgenlem  21404  qtopeu  21567  hmphindis  21648  filconn  21734  ufildr  21782  alexsubALTlem3  21900  ptcmplem2  21904  cnextfres1  21919  icccmplem1  22672  disjabrex  29521  disjabrexf  29522  locfinref  30036  pstmfval  30067  esumval  30236  esumpfinval  30265  esumpfinvalf  30266  prsiga  30322  fiunelcarsg  30506  carsgclctunlem1  30507  carsggect  30508  indispconn  31342  fobigcup  32132  onsucsuccmpi  32567  bj-nuliotaALT  33145  mbfresfi  33586  heiborlem3  33742  prsal  40856  isomenndlem  41065
 Copyright terms: Public domain W3C validator