elmapfn - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > elmapfn		Structured version Visualization version GIF version

Theorem elmapfn 8882

Description: A mapping is a function with the appropriate domain. (Contributed by AV, 6-Apr-2019.)

**Assertion**
Ref	Expression
elmapfn	⊢ (𝐴 ∈ (𝐵 ↑_m 𝐶) → 𝐴 Fn 𝐶)

**Proof of Theorem elmapfn**
Step	Hyp	Ref	Expression
1		elmapi 8866	. 2 ⊢ (𝐴 ∈ (𝐵 ↑_m 𝐶) → 𝐴:𝐶⟶𝐵)
2	1	ffnd 6718	1 ⊢ (𝐴 ∈ (𝐵 ↑_m 𝐶) → 𝐴 Fn 𝐶)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∈ wcel 2098 Fn wfn 6538 (class class class)co 7416 ↑_m cmap 8843

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-sep 5294 ax-nul 5301 ax-pow 5359 ax-pr 5423 ax-un 7738

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ral 3052 df-rex 3061 df-rab 3420 df-v 3465 df-sbc 3769 df-csb 3885 df-dif 3942 df-un 3944 df-in 3946 df-ss 3956 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5227 df-id 5570 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-fv 6551 df-ov 7419 df-oprab 7420 df-mpo 7421 df-1st 7991 df-2nd 7992 df-map 8845

This theorem is referenced by: mapxpen 9166 fsuppmapnn0fiublem 13987 fsuppmapnn0fiub 13988 fsuppmapnn0fiub0 13990 suppssfz 13991 fsuppmapnn0ub 13992 frlmbas 21693 frlmsslsp 21734 eqmat 22344 matplusgcell 22353 matsubgcell 22354 matvscacell 22356 cramerlem1 22607 tmdgsum 24017 fmptco1f1o 32463 islinds5 33127 ellspds 33128 lbsdiflsp0 33381 matmpo 33461 1smat1 33462 actfunsnf1o 34293 actfunsnrndisj 34294 reprinfz1 34311 unccur 37133 matunitlindflem1 37146 matunitlindflem2 37147 poimirlem4 37154 poimirlem5 37155 poimirlem6 37156 poimirlem7 37157 poimirlem10 37160 poimirlem11 37161 poimirlem12 37162 poimirlem16 37166 poimirlem19 37169 poimirlem29 37179 poimirlem30 37180 poimirlem31 37181 broucube 37184 fsuppind 41888 ofoafo 42850 ofoaass 42854 ofoacom 42855 rfovcnvf1od 43499 dssmapnvod 43515 dssmapntrcls 43623 k0004lem3 43644 unirnmap 44645 unirnmapsn 44651 ssmapsn 44653 dvnprodlem1 45397 dvnprodlem3 45399 rrxsnicc 45751 ioorrnopnlem 45755 ovnsubaddlem1 46021 hoiqssbllem1 46073 iccpartrn 46833 iccpartf 46834 iccpartnel 46841 mndpsuppss 47547 mndpfsupp 47552 dflinc2 47590 lincsum 47609 lincresunit2 47658 2arymaptfo 47839 rrx2pnecoorneor 47900 rrx2linest 47927

	
		OSZAR »