| 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 4513 | . . 3 ⊢ ∀𝑥 ∈ ∅ 𝐴 ∈ V | |
| 2 | eqid 2737 | . . . 4 ⊢ (𝑥 ∈ ∅ ↦ 𝐴) = (𝑥 ∈ ∅ ↦ 𝐴) | |
| 3 | 2 | fnmpt 6708 | . . 3 ⊢ (∀𝑥 ∈ ∅ 𝐴 ∈ V → (𝑥 ∈ ∅ ↦ 𝐴) Fn ∅) |
| 4 | 1, 3 | ax-mp 5 | . 2 ⊢ (𝑥 ∈ ∅ ↦ 𝐴) Fn ∅ |
| 5 | fn0 6699 | . 2 ⊢ ((𝑥 ∈ ∅ ↦ 𝐴) Fn ∅ ↔ (𝑥 ∈ ∅ ↦ 𝐴) = ∅) | |
| 6 | 4, 5 | mpbi 230 | 1 ⊢ (𝑥 ∈ ∅ ↦ 𝐴) = ∅ |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ∈ wcel 2108 ∀wral 3061 Vcvv 3480 ∅c0 4333 ↦ cmpt 5225 Fn wfn 6556 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-br 5144 df-opab 5206 df-mpt 5226 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-fun 6563 df-fn 6564 |
| This theorem is referenced by: oarec 8600 swrd00 14682 swrdlend 14691 repswswrd 14822 0rest 17474 grpinvfval 18996 grpinvfvalALT 18997 mulgnn0gsum 19098 psgnfval 19518 odfval 19550 odfvalALT 19551 gsumconst 19952 gsum2dlem2 19989 dprd0 20051 staffval 20842 gsumfsum 21452 pjfval 21726 asclfval 21899 mplcoe1 22055 mplcoe5 22058 coe1fzgsumd 22308 evl1gsumd 22361 mavmul0 22558 submafval 22585 mdetfval 22592 nfimdetndef 22595 mdetfval1 22596 mdet0pr 22598 madufval 22643 madugsum 22649 minmar1fval 22652 cramer0 22696 nmfval 24601 mdegfval 26101 of0r 32688 mptiffisupp 32702 gsumvsca1 33232 gsumvsca2 33233 elrgspnlem4 33249 esumnul 34049 esumrnmpt2 34069 sitg0 34348 mrsubfval 35513 msubfval 35529 elmsubrn 35533 mvhfval 35538 msrfval 35542 matunitlindflem1 37623 matunitlindf 37625 poimirlem28 37655 evl1gprodd 42118 idomnnzgmulnz 42134 deg1gprod 42141 sticksstones11 42157 liminf0 45808 cncfiooicc 45909 itgvol0 45983 stoweidlem9 46024 sge0iunmptlemfi 46428 sge0isum 46442 lincval0 48332 |
| Copyright terms: Public domain | W3C validator |