Theorem sneqbg 4845

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ∈ wcel 2107  {csn 4629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-sn 4630

This theorem is referenced by:  iotaval2  6512  suppval1  8152  suppsnop  8163  fseqdom  10021  infpwfidom  10023  canthwe  10646  s111  14565  initoid  17951  termoid  17952  embedsetcestrclem  18109  mat1dimelbas  21973  mat1dimbas  21974  unidifsnne  31804  altopthg  34970  altopthbg  34971  bj-snglc  35898  f1omptsnlem  36265  fvineqsnf1  36339  suceqsneq  37151  extid  37227  sn-iotalem  41086  eusnsn  45784