Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 0fv | Structured version Visualization version GIF version |
Description: Function value of the empty set. (Contributed by Stefan O'Rear, 26-Nov-2014.) |
Ref | Expression |
---|---|
0fv | ⊢ (∅‘𝐴) = ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | noel 4293 | . . 3 ⊢ ¬ 𝐴 ∈ ∅ | |
2 | dm0 5783 | . . . 4 ⊢ dom ∅ = ∅ | |
3 | 2 | eleq2i 2901 | . . 3 ⊢ (𝐴 ∈ dom ∅ ↔ 𝐴 ∈ ∅) |
4 | 1, 3 | mtbir 324 | . 2 ⊢ ¬ 𝐴 ∈ dom ∅ |
5 | ndmfv 6693 | . 2 ⊢ (¬ 𝐴 ∈ dom ∅ → (∅‘𝐴) = ∅) | |
6 | 4, 5 | ax-mp 5 | 1 ⊢ (∅‘𝐴) = ∅ |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 = wceq 1528 ∈ wcel 2105 ∅c0 4288 dom cdm 5548 ‘cfv 6348 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-nul 5201 ax-pow 5257 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2615 df-eu 2647 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rex 3141 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4831 df-br 5058 df-dm 5558 df-iota 6307 df-fv 6356 |
This theorem is referenced by: fv2prc 6703 csbfv12 6706 0ov 7182 csbov123 7187 csbov 7188 elovmpt3imp 7391 bropopvvv 7774 bropfvvvvlem 7775 itunisuc 9829 ccat1st1st 13972 str0 16523 ressbas 16542 cntrval 18387 cntzval 18389 cntzrcl 18395 rlmval 19892 opsrle 20184 opsrbaslem 20186 mpfrcl 20226 evlval 20236 psr1val 20282 vr1val 20288 chrval 20600 ocvval 20739 elocv 20740 iscnp2 21775 resvsca 30830 mrsubfval 32652 msubfval 32668 poimirlem28 34801 0cnv 41899 |
Copyright terms: Public domain | W3C validator |