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  8111  suppsnop  8123  fseqdom  9941  infpwfidom  9943  canthwe  10567  s111  14544  initoid  17930  termoid  17931  embedsetcestrclem  18085  mat1dimelbas  22420  mat1dimbas  22421  unidifsnne  32615  altopthg  36174  altopthbg  36175  bj-snglc  37183  f1omptsnlem  37554  fvineqsnf1  37628  extid  38530  suceqsneq  38698  qmapeldisjsim  39074  sn-iotalem  42556  eusnsn  47349