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

Theorem sneqbg 4845
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 4841 . 2 (𝐴𝑉 → ({𝐴} = {𝐵} → 𝐴 = 𝐵))
2 sneq 4639 . 2 (𝐴 = 𝐵 → {𝐴} = {𝐵})
31, 2impbid1 224 1 (𝐴𝑉 → ({𝐴} = {𝐵} ↔ 𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1539  wcel 2104  {csn 4629
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-sn 4630
This theorem is referenced by:  iotaval2  6512  suppval1  8156  suppsnop  8167  fseqdom  10025  infpwfidom  10027  canthwe  10650  s111  14571  initoid  17957  termoid  17958  embedsetcestrclem  18115  mat1dimelbas  22195  mat1dimbas  22196  unidifsnne  32038  altopthg  35241  altopthbg  35242  bj-snglc  36155  f1omptsnlem  36522  fvineqsnf1  36596  suceqsneq  37408  extid  37484  sn-iotalem  41346  eusnsn  46036
  Copyright terms: Public domain W3C validator