Theorem sneqbg 4776

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

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

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 4558

This theorem is referenced by:  iotaval2  6458  suppval1  8105  suppsnop  8117  fseqdom  9937  infpwfidom  9939  canthwe  10563  s111  14567  initoid  17957  termoid  17958  embedsetcestrclem  18112  mat1dimelbas  22424  mat1dimbas  22425  unidifsnne  32594  altopthg  36137  altopthbg  36138  bj-snglc  37264  f1omptsnlem  37640  fvineqsnf1  37714  extid  38625  suceqsneq  38793  qmapeldisjsim  39169  sn-iotalem  42650  eusnsn  47462