![]() |
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 4839 | . 2 ⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} → 𝐴 = 𝐵)) | |
2 | sneq 4634 | . 2 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) | |
3 | 1, 2 | impbid1 224 | 1 ⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} ↔ 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1534 ∈ wcel 2099 {csn 4624 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-sn 4625 |
This theorem is referenced by: iotaval2 6512 suppval1 8170 suppsnop 8182 fseqdom 10060 infpwfidom 10062 canthwe 10683 s111 14616 initoid 18016 termoid 18017 embedsetcestrclem 18174 mat1dimelbas 22459 mat1dimbas 22460 unidifsnne 32460 altopthg 35802 altopthbg 35803 bj-snglc 36687 f1omptsnlem 37054 fvineqsnf1 37128 suceqsneq 37945 extid 38019 sn-iotalem 41963 eusnsn 46675 |
Copyright terms: Public domain | W3C validator |