![]() |
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 2187 | . . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵)) | |
2 | 1 | abbidv 2295 | . 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵}) |
3 | df-sn 3597 | . 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴} | |
4 | df-sn 3597 | . 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵} | |
5 | 2, 3, 4 | 3eqtr4g 2235 | 1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1353 {cab 2163 {csn 3591 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-11 1506 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-sn 3597 |
This theorem is referenced by: sneqi 3603 sneqd 3604 euabsn 3661 absneu 3663 preq1 3668 tpeq3 3679 snssgOLD 3727 sneqrg 3760 sneqbg 3761 opeq1 3776 unisng 3824 exmidsssn 4199 exmidsssnc 4200 suceq 4398 snnex 4444 opeliunxp 4677 relop 4772 elimasng 4991 dmsnsnsng 5101 elxp4 5111 elxp5 5112 iotajust 5172 fconstg 5407 f1osng 5497 nfvres 5543 fsng 5684 fnressn 5697 fressnfv 5698 funfvima3 5744 isoselem 5814 1stvalg 6136 2ndvalg 6137 2ndval2 6150 fo1st 6151 fo2nd 6152 f1stres 6153 f2ndres 6154 mpomptsx 6191 dmmpossx 6193 fmpox 6194 brtpos2 6245 dftpos4 6257 tpostpos 6258 eceq1 6563 fvdiagfn 6686 mapsncnv 6688 elixpsn 6728 ixpsnf1o 6729 ensn1g 6790 en1 6792 xpsneng 6815 xpcomco 6819 xpassen 6823 xpdom2 6824 phplem3 6847 phplem3g 6849 fidifsnen 6863 xpfi 6922 pm54.43 7182 cc2lem 7243 cc2 7244 exp3val 10495 fsum2dlemstep 11413 fsumcnv 11416 fisumcom2 11417 fprod2dlemstep 11601 fprodcnv 11604 fprodcom2fi 11605 txswaphmeolem 13453 |
Copyright terms: Public domain | W3C validator |