![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > s1fv | Structured version Visualization version GIF 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 | ⊢ (𝐴 ∈ 𝐵 → (〈“𝐴”〉‘0) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | s1val 13694 | . . 3 ⊢ (𝐴 ∈ 𝐵 → 〈“𝐴”〉 = {〈0, 𝐴〉}) | |
2 | 1 | fveq1d 6450 | . 2 ⊢ (𝐴 ∈ 𝐵 → (〈“𝐴”〉‘0) = ({〈0, 𝐴〉}‘0)) |
3 | 0nn0 11664 | . . 3 ⊢ 0 ∈ ℕ0 | |
4 | fvsng 6715 | . . 3 ⊢ ((0 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵) → ({〈0, 𝐴〉}‘0) = 𝐴) | |
5 | 3, 4 | mpan 680 | . 2 ⊢ (𝐴 ∈ 𝐵 → ({〈0, 𝐴〉}‘0) = 𝐴) |
6 | 2, 5 | eqtrd 2814 | 1 ⊢ (𝐴 ∈ 𝐵 → (〈“𝐴”〉‘0) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1601 ∈ wcel 2107 {csn 4398 〈cop 4404 ‘cfv 6137 0cc0 10274 ℕ0cn0 11647 〈“cs1 13691 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5019 ax-nul 5027 ax-pr 5140 ax-1cn 10332 ax-icn 10333 ax-addcl 10334 ax-mulcl 10336 ax-i2m1 10342 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-sbc 3653 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4674 df-br 4889 df-opab 4951 df-id 5263 df-xp 5363 df-rel 5364 df-cnv 5365 df-co 5366 df-dm 5367 df-iota 6101 df-fun 6139 df-fv 6145 df-n0 11648 df-s1 13692 |
This theorem is referenced by: lsws1 13707 eqs1 13708 wrdl1s1 13710 ccats1val2 13723 ccat1st1st 13724 ccat2s1p1 13725 ccat2s1p2 13726 cats1un 13847 revs1 13917 cats1fvn 14015 s2fv0 14044 efgsval2 18541 efgs1 18543 efgsp1 18545 efgsfo 18548 pgpfaclem1 18878 loopclwwlkn1b 27449 clwwlkn1loopb 27450 clwwlknon1 27516 0wlkons1 27541 1wlkdlem4 27560 wlk2v2elem2 27576 signstf0 31253 signstfvn 31254 signsvtn0 31255 signsvtn0OLD 31256 signstfvneq0 31258 |
Copyright terms: Public domain | W3C validator |