![]() |
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 5312 | . . 3 ⊢ ∅ ∈ V | |
2 | str0.a | . . 3 ⊢ 𝐹 = Slot 𝐼 | |
3 | 1, 2 | strfvn 17188 | . 2 ⊢ (𝐹‘∅) = (∅‘𝐼) |
4 | 0fv 6945 | . 2 ⊢ (∅‘𝐼) = ∅ | |
5 | 3, 4 | eqtr2i 2755 | 1 ⊢ ∅ = (𝐹‘∅) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 ∅c0 4325 ‘cfv 6554 Slot cslot 17183 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-sep 5304 ax-nul 5311 ax-pr 5433 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-ral 3052 df-rex 3061 df-rab 3420 df-v 3464 df-dif 3950 df-un 3952 df-ss 3964 df-nul 4326 df-if 4534 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4914 df-br 5154 df-opab 5216 df-mpt 5237 df-id 5580 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-iota 6506 df-fun 6556 df-fv 6562 df-slot 17184 |
This theorem is referenced by: strfvi 17192 setsnid 17211 setsnidOLD 17212 base0 17218 resseqnbas 17255 resslemOLD 17256 oppchomfval 17727 oppchomfvalOLD 17728 fuchom 17985 fuchomOLD 17986 xpchomfval 18203 xpccofval 18206 oduleval 18314 0pos 18346 0posOLD 18347 frmdplusg 18844 efmndplusg 18870 oppgplusfval 19342 mgpplusg 20121 opprmulfval 20318 sralem 21154 sralemOLD 21155 srasca 21162 srascaOLD 21163 sravsca 21164 sravscaOLD 21165 sraip 21166 zlmlem 21506 zlmlemOLD 21507 zlmvsca 21515 thlle 21694 thlleOLD 21695 thloc 21697 psrplusg 21945 psrmulr 21951 psrvscafval 21957 opsrle 22054 ply1plusgfvi 22231 psr1sca2 22240 ply1sca2 22243 resstopn 23181 tnglem 24640 tnglemOLD 24641 tngds 24655 tngdsOLD 24656 ttglem 28804 ttglemOLD 28805 iedgval0 28976 resvlem 33205 resvlemOLD 33206 mendplusgfval 42846 mendmulrfval 42848 mendsca 42850 mendvscafval 42851 |
Copyright terms: Public domain | W3C validator |