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

Theorem sneqbg 4507
 Description: Two singletons of sets are equal iff their elements are equal. (Contributed by Scott Fenton, 16-Apr-2012.)
Assertion
Ref Expression
sneqbg (𝐴𝑉 → ({𝐴} = {𝐵} ↔ 𝐴 = 𝐵))

Proof of Theorem sneqbg
StepHypRef Expression
1 sneqrg 4503 . 2 (𝐴𝑉 → ({𝐴} = {𝐵} → 𝐴 = 𝐵))
2 sneq 4319 . 2 (𝐴 = 𝐵 → {𝐴} = {𝐵})
31, 2impbid1 215 1 (𝐴𝑉 → ({𝐴} = {𝐵} ↔ 𝐴 = 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   = wceq 1620   ∈ wcel 2127  {csn 4309 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-v 3330  df-sn 4310 This theorem is referenced by:  suppval1  7457  suppsnop  7465  fseqdom  9010  infpwfidom  9012  canthwe  9636  s111  13557  initoid  16827  termoid  16828  embedsetcestrclem  16969  mat1dimelbas  20450  mat1dimbas  20451  altopthg  32351  altopthbg  32352  bj-snglc  33234  f1omptsnlem  33465  extid  34374
 Copyright terms: Public domain W3C validator