Theorem sneqbg 4798

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {csn 4579

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-sn 4580

This theorem is referenced by:  iotaval2  6462  suppval1  8108  suppsnop  8120  fseqdom  9938  infpwfidom  9940  canthwe  10564  s111  14541  initoid  17927  termoid  17928  embedsetcestrclem  18082  mat1dimelbas  22417  mat1dimbas  22418  unidifsnne  32591  altopthg  36140  altopthbg  36141  bj-snglc  37143  f1omptsnlem  37510  fvineqsnf1  37584  extid  38486  suceqsneq  38654  qmapeldisjsim  39030  sn-iotalem  42515  eusnsn  47309