Theorem sneqbg 4803

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {csn 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-sn 4586

This theorem is referenced by:  iotaval2  6467  suppval1  8122  suppsnop  8134  fseqdom  9955  infpwfidom  9957  canthwe  10580  s111  14556  initoid  17943  termoid  17944  embedsetcestrclem  18098  mat1dimelbas  22391  mat1dimbas  22392  unidifsnne  32515  altopthg  35948  altopthbg  35949  bj-snglc  36950  f1omptsnlem  37317  fvineqsnf1  37391  suceqsneq  38218  extid  38291  sn-iotalem  42202  eusnsn  47020