Theorem sneqbg 4806

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

Step	Hyp	Ref	Expression
1		sneqrg 4802	. 2 ⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} → 𝐴 = 𝐵))
2		sneq 4597	. 2 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	impbid1 228	1 ⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} ↔ 𝐴 = 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  {csn 4587

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-sn 4588

This theorem is used by:  iotaval2  6508  suppval1  8167  suppsnop  8179  fseqdom  10032  infpwfidom  10034  canthwe  10663  s111  14685  initoid  18094  termoid  18095  embedsetcestrclem  18249  mat1dimelbas  22694  mat1dimbas  22695  unidifsnne  32997  selvply1rhmlem2  34018  altopthg  36534  altopthbg  36535  bj-snglc  37700  f1omptsnlem  38077  fvineqsnf1  38151  extid  39051  suceqsneq  39219  qmapeldisjsim  39595  sn-iotalem  43078  eusnsn  47901