Theorem sneqbg 4802

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  {csn 4583

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-sn 4584

This theorem is used by:  iotaval2  6498  suppval1  8161  suppsnop  8173  fseqdom  10076  infpwfidom  10078  canthwe  10707  s111  14730  initoid  18137  termoid  18138  embedsetcestrclem  18292  mat1dimelbas  22747  mat1dimbas  22748  unidifsnne  33065  selvply1rhmlem2  34086  altopthg  36654  altopthbg  36655  bj-snglc  37804  f1omptsnlem  38179  fvineqsnf1  38253  extid  39168  suceqsneq  39336  qmapeldisjsim  39712  sn-iotalem  43195  eusnsn  48018