Theorem sneqbg 4807

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1568   ∈ wcel 2141  {csn 4588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-sn 4589

This theorem is referenced by:  iotaval2  6507  suppval1  8161  suppsnop  8173  fseqdom  10009  infpwfidom  10011  canthwe  10635  s111  14652  initoid  18057  termoid  18058  embedsetcestrclem  18212  mat1dimelbas  22607  mat1dimbas  22608  unidifsnne  32848  selvply1rhmlem2  33877  altopthg  36413  altopthbg  36414  bj-snglc  37549  f1omptsnlem  37926  fvineqsnf1  38000  extid  38911  suceqsneq  39079  qmapeldisjsim  39455  sn-iotalem  42938  eusnsn  47708