Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sneq | GIF version |
Description: Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
sneq | ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq2 2147 | . . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵)) | |
2 | 1 | abbidv 2255 | . 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵}) |
3 | df-sn 3528 | . 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴} | |
4 | df-sn 3528 | . 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵} | |
5 | 2, 3, 4 | 3eqtr4g 2195 | 1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1331 {cab 2123 {csn 3522 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-11 1484 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2124 df-cleq 2130 df-sn 3528 |
This theorem is referenced by: sneqi 3534 sneqd 3535 euabsn 3588 absneu 3590 preq1 3595 tpeq3 3606 snssg 3651 sneqrg 3684 sneqbg 3685 opeq1 3700 unisng 3748 exmidsssn 4120 exmidsssnc 4121 suceq 4319 snnex 4364 opeliunxp 4589 relop 4684 elimasng 4902 dmsnsnsng 5011 elxp4 5021 elxp5 5022 iotajust 5082 fconstg 5314 f1osng 5401 nfvres 5447 fsng 5586 fnressn 5599 fressnfv 5600 funfvima3 5644 isoselem 5714 1stvalg 6033 2ndvalg 6034 2ndval2 6047 fo1st 6048 fo2nd 6049 f1stres 6050 f2ndres 6051 mpomptsx 6088 dmmpossx 6090 fmpox 6091 brtpos2 6141 dftpos4 6153 tpostpos 6154 eceq1 6457 fvdiagfn 6580 mapsncnv 6582 elixpsn 6622 ixpsnf1o 6623 ensn1g 6684 en1 6686 xpsneng 6709 xpcomco 6713 xpassen 6717 xpdom2 6718 phplem3 6741 phplem3g 6743 fidifsnen 6757 xpfi 6811 pm54.43 7039 exp3val 10288 fsum2dlemstep 11196 fsumcnv 11199 fisumcom2 11200 txswaphmeolem 12478 |
Copyright terms: Public domain | W3C validator |