Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mpt0 | Structured version Visualization version GIF version |
Description: A mapping operation with empty domain. (Contributed by Mario Carneiro, 28-Dec-2014.) |
Ref | Expression |
---|---|
mpt0 | ⊢ (𝑥 ∈ ∅ ↦ 𝐴) = ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ral0 4454 | . . 3 ⊢ ∀𝑥 ∈ ∅ 𝐴 ∈ V | |
2 | eqid 2821 | . . . 4 ⊢ (𝑥 ∈ ∅ ↦ 𝐴) = (𝑥 ∈ ∅ ↦ 𝐴) | |
3 | 2 | fnmpt 6482 | . . 3 ⊢ (∀𝑥 ∈ ∅ 𝐴 ∈ V → (𝑥 ∈ ∅ ↦ 𝐴) Fn ∅) |
4 | 1, 3 | ax-mp 5 | . 2 ⊢ (𝑥 ∈ ∅ ↦ 𝐴) Fn ∅ |
5 | fn0 6473 | . 2 ⊢ ((𝑥 ∈ ∅ ↦ 𝐴) Fn ∅ ↔ (𝑥 ∈ ∅ ↦ 𝐴) = ∅) | |
6 | 4, 5 | mpbi 231 | 1 ⊢ (𝑥 ∈ ∅ ↦ 𝐴) = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 ∈ wcel 2105 ∀wral 3138 Vcvv 3495 ∅c0 4290 ↦ cmpt 5138 Fn wfn 6344 |
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 2793 ax-sep 5195 ax-nul 5202 ax-pr 5321 |
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 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3497 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-br 5059 df-opab 5121 df-mpt 5139 df-id 5454 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-fun 6351 df-fn 6352 |
This theorem is referenced by: oarec 8178 swrd00 13996 swrdlend 14005 repswswrd 14136 0rest 16693 grpinvfval 18082 grpinvfvalALT 18083 mulgnn0gsum 18174 psgnfval 18559 odfval 18591 odfvalALT 18592 gsumconst 18985 gsum2dlem2 19022 dprd0 19084 staffval 19549 asclfval 20038 mplcoe1 20176 mplcoe5 20179 coe1fzgsumd 20400 evl1gsumd 20450 gsumfsum 20542 pjfval 20780 mavmul0 21091 submafval 21118 mdetfval 21125 nfimdetndef 21128 mdetfval1 21129 mdet0pr 21131 madufval 21176 madugsum 21182 minmar1fval 21185 cramer0 21229 nmfval 23127 mdegfval 24585 gsumvsca1 30782 gsumvsca2 30783 esumnul 31207 esumrnmpt2 31227 sitg0 31504 mrsubfval 32653 msubfval 32669 elmsubrn 32673 mvhfval 32678 msrfval 32682 matunitlindflem1 34770 matunitlindf 34772 poimirlem28 34802 liminf0 41954 cncfiooicc 42057 itgvol0 42133 stoweidlem9 42175 sge0iunmptlemfi 42576 sge0isum 42590 lincval0 44368 |
Copyright terms: Public domain | W3C validator |