| 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 4636 | . 2 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) | |
| 3 | 1, 2 | impbid1 225 | 1 ⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} ↔ 𝐴 = 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ∈ wcel 2108 {csn 4626 |
| 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 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-sn 4627 |
| This theorem is referenced by: iotaval2 6529 suppval1 8191 suppsnop 8203 fseqdom 10066 infpwfidom 10068 canthwe 10691 s111 14653 initoid 18046 termoid 18047 embedsetcestrclem 18202 mat1dimelbas 22477 mat1dimbas 22478 unidifsnne 32554 altopthg 35968 altopthbg 35969 bj-snglc 36970 f1omptsnlem 37337 fvineqsnf1 37411 suceqsneq 38238 extid 38311 sn-iotalem 42260 eusnsn 47038 |
| Copyright terms: Public domain | W3C validator |