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

Theorem sneqbg 4848
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 4844 . 2 (𝐴𝑉 → ({𝐴} = {𝐵} → 𝐴 = 𝐵))
2 sneq 4641 . 2 (𝐴 = 𝐵 → {𝐴} = {𝐵})
31, 2impbid1 225 1 (𝐴𝑉 → ({𝐴} = {𝐵} ↔ 𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1537  wcel 2106  {csn 4631
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-sn 4632
This theorem is referenced by:  iotaval2  6531  suppval1  8190  suppsnop  8202  fseqdom  10064  infpwfidom  10066  canthwe  10689  s111  14650  initoid  18055  termoid  18056  embedsetcestrclem  18213  mat1dimelbas  22493  mat1dimbas  22494  unidifsnne  32562  altopthg  35949  altopthbg  35950  bj-snglc  36952  f1omptsnlem  37319  fvineqsnf1  37393  suceqsneq  38218  extid  38292  sn-iotalem  42239  eusnsn  46976
  Copyright terms: Public domain W3C validator