Theorem sneqbg 4803

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1562   ∈ wcel 2144  {csn 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-sn 4585

This theorem is referenced by:  iotaval2  6494  suppval1  8148  suppsnop  8160  fseqdom  9984  infpwfidom  9986  canthwe  10611  s111  14631  initoid  18036  termoid  18037  embedsetcestrclem  18191  mat1dimelbas  22533  mat1dimbas  22534  unidifsnne  32737  selvply1rhmlem2  33820  altopthg  36322  altopthbg  36323  bj-snglc  37459  f1omptsnlem  37835  fvineqsnf1  37909  extid  38820  suceqsneq  38988  qmapeldisjsim  39364  sn-iotalem  42845  eusnsn  47625