Theorem sneqbg 4868

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2108  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-sn 4649

This theorem is referenced by:  iotaval2  6541  suppval1  8207  suppsnop  8219  fseqdom  10095  infpwfidom  10097  canthwe  10720  s111  14663  initoid  18068  termoid  18069  embedsetcestrclem  18226  mat1dimelbas  22498  mat1dimbas  22499  unidifsnne  32564  altopthg  35931  altopthbg  35932  bj-snglc  36935  f1omptsnlem  37302  fvineqsnf1  37376  suceqsneq  38192  extid  38266  sn-iotalem  42214  eusnsn  46941