![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sneqbg | Structured version Visualization version GIF version |
Description: Two singletons of sets are equal iff their elements are equal. (Contributed by Scott Fenton, 16-Apr-2012.) |
Ref | Expression |
---|---|
sneqbg | ⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} ↔ 𝐴 = 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sneqrg 4844 | . 2 ⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} → 𝐴 = 𝐵)) | |
2 | sneq 4641 | . 2 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) | |
3 | 1, 2 | impbid1 225 | 1 ⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} ↔ 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 = wceq 1537 ∈ wcel 2106 {csn 4631 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-sn 4632 |
This theorem is referenced by: iotaval2 6531 suppval1 8190 suppsnop 8202 fseqdom 10064 infpwfidom 10066 canthwe 10689 s111 14650 initoid 18055 termoid 18056 embedsetcestrclem 18213 mat1dimelbas 22493 mat1dimbas 22494 unidifsnne 32562 altopthg 35949 altopthbg 35950 bj-snglc 36952 f1omptsnlem 37319 fvineqsnf1 37393 suceqsneq 38218 extid 38292 sn-iotalem 42239 eusnsn 46976 |
Copyright terms: Public domain | W3C validator |