Theorem elmapfn 8653

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 8637	. 2 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → 𝐴:𝐶⟶𝐵)
2	1	ffnd 6601	1 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → 𝐴 Fn 𝐶)

Syntax hints:   → wi 4   ∈ wcel 2106   Fn wfn 6428  (class class class)co 7275   ↑_m cmap 8615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280  df-1st 7831  df-2nd 7832  df-map 8617

This theorem is referenced by:  mapxpen  8930  fsuppmapnn0fiublem  13710  fsuppmapnn0fiub  13711  fsuppmapnn0fiub0  13713  suppssfz  13714  fsuppmapnn0ub  13715  frlmbas  20962  frlmsslsp  21003  eqmat  21573  matplusgcell  21582  matsubgcell  21583  matvscacell  21585  cramerlem1  21836  tmdgsum  23246  fmptco1f1o  30968  islinds5  31563  ellspds  31564  lbsdiflsp0  31707  matmpo  31753  1smat1  31754  actfunsnf1o  32584  actfunsnrndisj  32585  reprinfz1  32602  unccur  35760  matunitlindflem1  35773  matunitlindflem2  35774  poimirlem4  35781  poimirlem5  35782  poimirlem6  35783  poimirlem7  35784  poimirlem10  35787  poimirlem11  35788  poimirlem12  35789  poimirlem16  35793  poimirlem19  35796  poimirlem29  35806  poimirlem30  35807  poimirlem31  35808  broucube  35811  fsuppind  40279  rfovcnvf1od  41612  dssmapnvod  41628  dssmapntrcls  41738  k0004lem3  41759  unirnmap  42748  unirnmapsn  42754  ssmapsn  42756  dvnprodlem1  43487  dvnprodlem3  43489  rrxsnicc  43841  ioorrnopnlem  43845  ovnsubaddlem1  44108  hoiqssbllem1  44160  iccpartrn  44882  iccpartf  44883  iccpartnel  44890  mndpsuppss  45707  mndpfsupp  45712  dflinc2  45751  lincsum  45770  lincresunit2  45819  2arymaptfo  46000  rrx2pnecoorneor  46061  rrx2linest  46088