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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106  {csn 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-sn 4592

This theorem is referenced by:  iotaval2  6469  suppval1  8103  suppsnop  8114  fseqdom  9971  infpwfidom  9973  canthwe  10596  s111  14515  initoid  17901  termoid  17902  embedsetcestrclem  18059  mat1dimelbas  21857  mat1dimbas  21858  unidifsnne  31527  altopthg  34628  altopthbg  34629  bj-snglc  35513  f1omptsnlem  35880  fvineqsnf1  35954  suceqsneq  36767  extid  36844  sn-iotalem  40714  eusnsn  45380