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 3878 | . . 3 ⊢ ¬ 𝐴 ∈ ∅ | |
2 | dm0 5260 | . . . 4 ⊢ dom ∅ = ∅ | |
3 | 2 | eleq2i 2680 | . . 3 ⊢ (𝐴 ∈ dom ∅ ↔ 𝐴 ∈ ∅) |
4 | 1, 3 | mtbir 312 | . 2 ⊢ ¬ 𝐴 ∈ dom ∅ |
5 | ndmfv 6128 | . 2 ⊢ (¬ 𝐴 ∈ dom ∅ → (∅‘𝐴) = ∅) | |
6 | 4, 5 | ax-mp 5 | 1 ⊢ (∅‘𝐴) = ∅ |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 = wceq 1475 ∈ wcel 1977 ∅c0 3874 dom cdm 5038 ‘cfv 5804 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-nul 4717 ax-pow 4769 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-dm 5048 df-iota 5768 df-fv 5812 |
This theorem is referenced by: fv2prc 6138 csbfv12 6141 0ov 6580 csbov123 6585 csbov 6586 elovmpt3imp 6788 bropopvvv 7142 bropfvvvvlem 7143 itunisuc 9124 itunitc1 9125 str0 15739 ressbas 15757 cntrval 17575 cntzval 17577 cntzrcl 17583 sralem 18998 srasca 19002 sravsca 19003 sraip 19004 rlmval 19012 opsrle 19296 opsrbaslem 19298 opsrbaslemOLD 19299 mpfrcl 19339 evlval 19345 psr1val 19377 vr1val 19383 chrval 19692 ocvval 19830 elocv 19831 iscnp2 20853 clwwlkgt0 26299 clwwlknprop 26300 resvsca 29161 mrsubfval 30659 msubfval 30675 poimirlem28 32607 |
Copyright terms: Public domain | W3C validator |