Theorem sneqbg 4787

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540   ∈ wcel 2105  {csn 4572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-sn 4573

This theorem is referenced by:  iotaval2  6441  suppval1  8045  suppsnop  8056  fseqdom  9875  infpwfidom  9877  canthwe  10500  s111  14411  initoid  17805  termoid  17806  embedsetcestrclem  17963  mat1dimelbas  21718  mat1dimbas  21719  unidifsnne  31112  altopthg  34360  altopthbg  34361  bj-snglc  35248  f1omptsnlem  35605  fvineqsnf1  35679  suceqsneq  36492  extid  36569  sn-iotalem  40440  eusnsn  44860