![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > str0 | Structured version Visualization version GIF version |
Description: All components of the empty set are empty sets. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 7-Dec-2014.) |
Ref | Expression |
---|---|
str0.a | ⊢ 𝐹 = Slot 𝐼 |
Ref | Expression |
---|---|
str0 | ⊢ ∅ = (𝐹‘∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0ex 5013 | . . 3 ⊢ ∅ ∈ V | |
2 | str0.a | . . 3 ⊢ 𝐹 = Slot 𝐼 | |
3 | 1, 2 | strfvn 16243 | . 2 ⊢ (𝐹‘∅) = (∅‘𝐼) |
4 | 0fv 6472 | . 2 ⊢ (∅‘𝐼) = ∅ | |
5 | 3, 4 | eqtr2i 2849 | 1 ⊢ ∅ = (𝐹‘∅) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1658 ∅c0 4143 ‘cfv 6122 Slot cslot 16220 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2390 ax-ext 2802 ax-sep 5004 ax-nul 5012 ax-pow 5064 ax-pr 5126 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2604 df-eu 2639 df-clab 2811 df-cleq 2817 df-clel 2820 df-nfc 2957 df-ral 3121 df-rex 3122 df-rab 3125 df-v 3415 df-sbc 3662 df-dif 3800 df-un 3802 df-in 3804 df-ss 3811 df-nul 4144 df-if 4306 df-sn 4397 df-pr 4399 df-op 4403 df-uni 4658 df-br 4873 df-opab 4935 df-mpt 4952 df-id 5249 df-xp 5347 df-rel 5348 df-cnv 5349 df-co 5350 df-dm 5351 df-iota 6085 df-fun 6124 df-fv 6130 df-slot 16225 |
This theorem is referenced by: base0 16274 strfvi 16275 setsnid 16277 resslem 16295 oppchomfval 16725 fuchom 16972 xpchomfval 17171 xpccofval 17174 0pos 17306 oduleval 17483 frmdplusg 17744 oppgplusfval 18127 symgplusg 18158 mgpplusg 18846 opprmulfval 18978 sralem 19537 srasca 19541 sravsca 19542 sraip 19543 psrplusg 19741 psrmulr 19744 psrvscafval 19750 opsrle 19835 ply1plusgfvi 19971 psr1sca2 19980 ply1sca2 19983 zlmlem 20224 zlmvsca 20229 thlle 20403 thloc 20405 resstopn 21360 tnglem 22813 tngds 22821 ttglem 26174 iedgval0 26337 resvlem 30375 mendplusgfval 38597 mendmulrfval 38599 mendsca 38601 mendvscafval 38602 |
Copyright terms: Public domain | W3C validator |