![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sneq | Unicode 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 2098 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | abbidv 2206 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | df-sn 3456 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | df-sn 3456 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | 3eqtr4g 2146 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
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 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-11 1443 ax-4 1446 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 |
This theorem depends on definitions: df-bi 116 df-tru 1293 df-nf 1396 df-sb 1694 df-clab 2076 df-cleq 2082 df-sn 3456 |
This theorem is referenced by: sneqi 3462 sneqd 3463 euabsn 3516 absneu 3518 preq1 3523 tpeq3 3534 snssg 3579 sneqrg 3612 sneqbg 3613 opeq1 3628 unisng 3676 exmidsssn 4040 suceq 4238 snnex 4283 opeliunxp 4506 relop 4599 elimasng 4813 dmsnsnsng 4921 elxp4 4931 elxp5 4932 iotajust 4992 fconstg 5220 f1osng 5307 nfvres 5350 fsng 5484 fnressn 5497 fressnfv 5498 funfvima3 5542 isoselem 5613 1stvalg 5927 2ndvalg 5928 2ndval2 5941 fo1st 5942 fo2nd 5943 f1stres 5944 f2ndres 5945 mpt2mptsx 5981 dmmpt2ssx 5983 fmpt2x 5984 brtpos2 6030 dftpos4 6042 tpostpos 6043 eceq1 6341 fvdiagfn 6464 mapsncnv 6466 elixpsn 6506 ixpsnf1o 6507 ensn1g 6568 en1 6570 xpsneng 6592 xpcomco 6596 xpassen 6600 xpdom2 6601 phplem3 6624 phplem3g 6626 fidifsnen 6640 xpfi 6694 pm54.43 6879 exp3val 10018 fsum2dlemstep 10889 fsumcnv 10892 fisumcom2 10893 |
Copyright terms: Public domain | W3C validator |