Theorem elmapfn 8838

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

Syntax hints:   → wi 4   ∈ wcel 2109   Fn wfn 6506  (class class class)co 7387   ↑_m cmap 8799

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392  df-1st 7968  df-2nd 7969  df-map 8801

This theorem is referenced by:  mapxpen  9107  fsuppmapnn0fiublem  13955  fsuppmapnn0fiub  13956  fsuppmapnn0fiub0  13958  suppssfz  13959  fsuppmapnn0ub  13960  mndpsuppss  18692  mndpfsupp  18694  frlmbas  21664  frlmsslsp  21705  eqmat  22311  matplusgcell  22320  matsubgcell  22321  matvscacell  22323  cramerlem1  22574  tmdgsum  23982  fmptco1f1o  32557  islinds5  33338  ellspds  33339  1arithidomlem2  33507  1arithidom  33508  lbsdiflsp0  33622  matmpo  33793  1smat1  33794  actfunsnf1o  34595  actfunsnrndisj  34596  reprinfz1  34613  unccur  37597  matunitlindflem1  37610  matunitlindflem2  37611  poimirlem4  37618  poimirlem5  37619  poimirlem6  37620  poimirlem7  37621  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem16  37630  poimirlem19  37633  poimirlem29  37643  poimirlem30  37644  poimirlem31  37645  broucube  37648  fsuppind  42578  ofoafo  43345  ofoaass  43349  ofoacom  43350  rfovcnvf1od  43993  dssmapnvod  44009  dssmapntrcls  44117  k0004lem3  44138  unirnmap  45202  unirnmapsn  45208  ssmapsn  45210  dvnprodlem1  45944  dvnprodlem3  45946  rrxsnicc  46298  ioorrnopnlem  46302  ovnsubaddlem1  46568  hoiqssbllem1  46620  iccpartrn  47431  iccpartf  47432  iccpartnel  47439  dflinc2  48399  lincsum  48418  lincresunit2  48467  2arymaptfo  48643  rrx2pnecoorneor  48704  rrx2linest  48731