Theorem sneqbg 4800

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sn 4582

This theorem is referenced by:  iotaval2  6464  suppval1  8110  suppsnop  8122  fseqdom  9940  infpwfidom  9942  canthwe  10566  s111  14543  initoid  17929  termoid  17930  embedsetcestrclem  18084  mat1dimelbas  22419  mat1dimbas  22420  unidifsnne  32593  altopthg  36142  altopthbg  36143  bj-snglc  37145  f1omptsnlem  37512  fvineqsnf1  37586  extid  38488  suceqsneq  38656  qmapeldisjsim  39032  sn-iotalem  42514  eusnsn  47308