![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > s1fv | Structured version Unicode version |
Description: Sole symbol of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
Ref | Expression |
---|---|
s1fv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | s1val 12401 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | fveq1d 5794 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 0nn0 10698 |
. . 3
![]() ![]() ![]() ![]() | |
4 | fvsng 6014 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | mpan 670 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 2, 5 | eqtrd 2492 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-sep 4514 ax-nul 4522 ax-pr 4632 ax-1cn 9444 ax-icn 9445 ax-addcl 9446 ax-mulcl 9448 ax-i2m1 9454 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-ral 2800 df-rex 2801 df-rab 2804 df-v 3073 df-sbc 3288 df-dif 3432 df-un 3434 df-in 3436 df-ss 3443 df-nul 3739 df-if 3893 df-sn 3979 df-pr 3981 df-op 3985 df-uni 4193 df-br 4394 df-opab 4452 df-id 4737 df-xp 4947 df-rel 4948 df-cnv 4949 df-co 4950 df-dm 4951 df-iota 5482 df-fun 5521 df-fv 5527 df-n0 10684 df-s1 12343 |
This theorem is referenced by: lsws1 12410 eqs1 12411 wrdl1s1 12412 ccats1val2 12418 cats1un 12481 revs1 12516 cats1fvn 12596 s2fv0 12623 efgsval2 16343 efgs1 16345 efgsp1 16347 efgsfo 16349 pgpfaclem1 16696 signstf0 27106 signstfvn 27107 signsvtn0 27108 signstfvneq0 27110 ccat2s1p1 30406 ccat2s1p2 30407 |
Copyright terms: Public domain | W3C validator |