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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sn 4569

This theorem is referenced by:  iotaval2  6461  suppval1  8107  suppsnop  8119  fseqdom  9937  infpwfidom  9939  canthwe  10563  s111  14540  initoid  17926  termoid  17927  embedsetcestrclem  18081  mat1dimelbas  22414  mat1dimbas  22415  unidifsnne  32595  altopthg  36155  altopthbg  36156  bj-snglc  37274  f1omptsnlem  37648  fvineqsnf1  37722  extid  38628  suceqsneq  38796  qmapeldisjsim  39172  sn-iotalem  42654  eusnsn  47460