![]() |
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 2122 | . . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵)) | |
2 | 1 | abbidv 2230 | . 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵}) |
3 | df-sn 3497 | . 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴} | |
4 | df-sn 3497 | . 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵} | |
5 | 2, 3, 4 | 3eqtr4g 2170 | 1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1312 {cab 2099 {csn 3491 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1404 ax-7 1405 ax-gen 1406 ax-ie1 1450 ax-ie2 1451 ax-8 1463 ax-11 1465 ax-4 1468 ax-17 1487 ax-i9 1491 ax-ial 1495 ax-i5r 1496 ax-ext 2095 |
This theorem depends on definitions: df-bi 116 df-tru 1315 df-nf 1418 df-sb 1717 df-clab 2100 df-cleq 2106 df-sn 3497 |
This theorem is referenced by: sneqi 3503 sneqd 3504 euabsn 3557 absneu 3559 preq1 3564 tpeq3 3575 snssg 3620 sneqrg 3653 sneqbg 3654 opeq1 3669 unisng 3717 exmidsssn 4083 exmidsssnc 4084 suceq 4282 snnex 4327 opeliunxp 4552 relop 4647 elimasng 4863 dmsnsnsng 4972 elxp4 4982 elxp5 4983 iotajust 5043 fconstg 5275 f1osng 5362 nfvres 5406 fsng 5545 fnressn 5558 fressnfv 5559 funfvima3 5603 isoselem 5673 1stvalg 5992 2ndvalg 5993 2ndval2 6006 fo1st 6007 fo2nd 6008 f1stres 6009 f2ndres 6010 mpomptsx 6047 dmmpossx 6049 fmpox 6050 brtpos2 6100 dftpos4 6112 tpostpos 6113 eceq1 6416 fvdiagfn 6539 mapsncnv 6541 elixpsn 6581 ixpsnf1o 6582 ensn1g 6643 en1 6645 xpsneng 6667 xpcomco 6671 xpassen 6675 xpdom2 6676 phplem3 6699 phplem3g 6701 fidifsnen 6715 xpfi 6769 pm54.43 6993 exp3val 10182 fsum2dlemstep 11089 fsumcnv 11092 fisumcom2 11093 |
Copyright terms: Public domain | W3C validator |