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

Theorem sneqbg 4843
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 4839 . 2 (𝐴𝑉 → ({𝐴} = {𝐵} → 𝐴 = 𝐵))
2 sneq 4636 . 2 (𝐴 = 𝐵 → {𝐴} = {𝐵})
31, 2impbid1 225 1 (𝐴𝑉 → ({𝐴} = {𝐵} ↔ 𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1540  wcel 2108  {csn 4626
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-sn 4627
This theorem is referenced by:  iotaval2  6529  suppval1  8191  suppsnop  8203  fseqdom  10066  infpwfidom  10068  canthwe  10691  s111  14653  initoid  18046  termoid  18047  embedsetcestrclem  18202  mat1dimelbas  22477  mat1dimbas  22478  unidifsnne  32554  altopthg  35968  altopthbg  35969  bj-snglc  36970  f1omptsnlem  37337  fvineqsnf1  37411  suceqsneq  38238  extid  38311  sn-iotalem  42260  eusnsn  47038
  Copyright terms: Public domain W3C validator