Theorem sneqbg 4776

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1548   ∈ wcel 2121  {csn 4557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-sn 4558

This theorem is referenced by:  iotaval2  6459  suppval1  8108  suppsnop  8120  fseqdom  9943  infpwfidom  9945  canthwe  10570  s111  14573  initoid  17963  termoid  17964  embedsetcestrclem  18118  mat1dimelbas  22457  mat1dimbas  22458  unidifsnne  32626  selvply1rhmlem2  33715  altopthg  36208  altopthbg  36209  bj-snglc  37335  f1omptsnlem  37711  fvineqsnf1  37785  extid  38696  suceqsneq  38864  qmapeldisjsim  39240  sn-iotalem  42721  eusnsn  47501