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 2819 | . . . 4 ⊢ (𝑥 ∈ ∅ ↦ 𝐴) = (𝑥 ∈ ∅ ↦ 𝐴) | |
3 | 2 | fnmpt 6481 | . . 3 ⊢ (∀𝑥 ∈ ∅ 𝐴 ∈ V → (𝑥 ∈ ∅ ↦ 𝐴) Fn ∅) |
4 | 1, 3 | ax-mp 5 | . 2 ⊢ (𝑥 ∈ ∅ ↦ 𝐴) Fn ∅ |
5 | fn0 6472 | . 2 ⊢ ((𝑥 ∈ ∅ ↦ 𝐴) Fn ∅ ↔ (𝑥 ∈ ∅ ↦ 𝐴) = ∅) | |
6 | 4, 5 | mpbi 232 | 1 ⊢ (𝑥 ∈ ∅ ↦ 𝐴) = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1531 ∈ wcel 2108 ∀wral 3136 Vcvv 3493 ∅c0 4289 ↦ cmpt 5137 Fn wfn 6343 |
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 1905 ax-6 1964 ax-7 2009 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2154 ax-12 2170 ax-ext 2791 ax-sep 5194 ax-nul 5201 ax-pr 5320 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1084 df-tru 1534 df-ex 1775 df-nf 1779 df-sb 2064 df-mo 2616 df-eu 2648 df-clab 2798 df-cleq 2812 df-clel 2891 df-nfc 2961 df-ral 3141 df-rex 3142 df-rab 3145 df-v 3495 df-dif 3937 df-un 3939 df-in 3941 df-ss 3950 df-nul 4290 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-br 5058 df-opab 5120 df-mpt 5138 df-id 5453 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-fun 6350 df-fn 6351 |
This theorem is referenced by: oarec 8180 swrd00 13998 swrdlend 14007 repswswrd 14138 0rest 16695 grpinvfval 18134 grpinvfvalALT 18135 mulgnn0gsum 18226 psgnfval 18620 odfval 18652 odfvalALT 18653 gsumconst 19046 gsum2dlem2 19083 dprd0 19145 staffval 19610 asclfval 20100 mplcoe1 20238 mplcoe5 20241 coe1fzgsumd 20462 evl1gsumd 20512 gsumfsum 20604 pjfval 20842 mavmul0 21153 submafval 21180 mdetfval 21187 nfimdetndef 21190 mdetfval1 21191 mdet0pr 21193 madufval 21238 madugsum 21244 minmar1fval 21247 cramer0 21291 nmfval 23190 mdegfval 24648 gsumvsca1 30847 gsumvsca2 30848 esumnul 31300 esumrnmpt2 31320 sitg0 31597 mrsubfval 32748 msubfval 32764 elmsubrn 32768 mvhfval 32773 msrfval 32777 matunitlindflem1 34880 matunitlindf 34882 poimirlem28 34912 liminf0 42064 cncfiooicc 42167 itgvol0 42243 stoweidlem9 42285 sge0iunmptlemfi 42686 sge0isum 42700 lincval0 44461 |
Copyright terms: Public domain | W3C validator |