Theorem sneqbg 4802

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 4798	. 2 ⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} → 𝐴 = 𝐵))
2		sneq 4593	. 2 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	impbid1 228	1 ⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} ↔ 𝐴 = 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2144  {csn 4583

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-sn 4584

This theorem is used by:  iotaval2  6509  suppval1  8183  suppsnop  8195  fseqdom  10105  infpwfidom  10107  canthwe  10736  s111  14763  initoid  18176  termoid  18177  embedsetcestrclem  18331  mat1dimelbas  22786  mat1dimbas  22787  unidifsnne  33132  selvply1rhmlem2  34153  altopthg  36732  altopthbg  36733  bj-snglc  37882  f1omptsnlem  38260  fvineqsnf1  38334  extid  39249  suceqsneq  39417  qmapeldisjsim  39793  sn-iotalem  43276  eusnsn  48096