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 2174 | . . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵)) | |
2 | 1 | abbidv 2282 | . 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵}) |
3 | df-sn 3576 | . 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴} | |
4 | df-sn 3576 | . 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵} | |
5 | 2, 3, 4 | 3eqtr4g 2222 | 1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1342 {cab 2150 {csn 3570 |
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 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-11 1493 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-sn 3576 |
This theorem is referenced by: sneqi 3582 sneqd 3583 euabsn 3640 absneu 3642 preq1 3647 tpeq3 3658 snssg 3703 sneqrg 3736 sneqbg 3737 opeq1 3752 unisng 3800 exmidsssn 4175 exmidsssnc 4176 suceq 4374 snnex 4420 opeliunxp 4653 relop 4748 elimasng 4966 dmsnsnsng 5075 elxp4 5085 elxp5 5086 iotajust 5146 fconstg 5378 f1osng 5467 nfvres 5513 fsng 5652 fnressn 5665 fressnfv 5666 funfvima3 5712 isoselem 5782 1stvalg 6102 2ndvalg 6103 2ndval2 6116 fo1st 6117 fo2nd 6118 f1stres 6119 f2ndres 6120 mpomptsx 6157 dmmpossx 6159 fmpox 6160 brtpos2 6210 dftpos4 6222 tpostpos 6223 eceq1 6527 fvdiagfn 6650 mapsncnv 6652 elixpsn 6692 ixpsnf1o 6693 ensn1g 6754 en1 6756 xpsneng 6779 xpcomco 6783 xpassen 6787 xpdom2 6788 phplem3 6811 phplem3g 6813 fidifsnen 6827 xpfi 6886 pm54.43 7137 cc2lem 7198 cc2 7199 exp3val 10447 fsum2dlemstep 11361 fsumcnv 11364 fisumcom2 11365 fprod2dlemstep 11549 fprodcnv 11552 fprodcom2fi 11553 txswaphmeolem 12867 |
Copyright terms: Public domain | W3C validator |