![]() |
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 5015 | . . 3 ⊢ ∅ ∈ V | |
2 | str0.a | . . 3 ⊢ 𝐹 = Slot 𝐼 | |
3 | 1, 2 | strfvn 16245 | . 2 ⊢ (𝐹‘∅) = (∅‘𝐼) |
4 | 0fv 6474 | . 2 ⊢ (∅‘𝐼) = ∅ | |
5 | 3, 4 | eqtr2i 2851 | 1 ⊢ ∅ = (𝐹‘∅) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1658 ∅c0 4145 ‘cfv 6124 Slot cslot 16222 |
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 2391 ax-ext 2804 ax-sep 5006 ax-nul 5014 ax-pow 5066 ax-pr 5128 |
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 2606 df-eu 2641 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-ral 3123 df-rex 3124 df-rab 3127 df-v 3417 df-sbc 3664 df-dif 3802 df-un 3804 df-in 3806 df-ss 3813 df-nul 4146 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4660 df-br 4875 df-opab 4937 df-mpt 4954 df-id 5251 df-xp 5349 df-rel 5350 df-cnv 5351 df-co 5352 df-dm 5353 df-iota 6087 df-fun 6126 df-fv 6132 df-slot 16227 |
This theorem is referenced by: base0 16276 strfvi 16277 setsnid 16279 resslem 16297 oppchomfval 16727 fuchom 16974 xpchomfval 17173 xpccofval 17176 0pos 17308 oduleval 17485 frmdplusg 17746 oppgplusfval 18129 symgplusg 18160 mgpplusg 18848 opprmulfval 18980 sralem 19539 srasca 19543 sravsca 19544 sraip 19545 psrplusg 19743 psrmulr 19746 psrvscafval 19752 opsrle 19837 ply1plusgfvi 19973 psr1sca2 19982 ply1sca2 19985 zlmlem 20226 zlmvsca 20231 thlle 20405 thloc 20407 resstopn 21362 tnglem 22815 tngds 22823 ttglem 26176 iedgval0 26339 resvlem 30377 mendplusgfval 38599 mendmulrfval 38601 mendsca 38603 mendvscafval 38604 |
Copyright terms: Public domain | W3C validator |