Theorem elmapfn 8814

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

Syntax hints:   → wi 4   ∈ wcel 2114   Fn wfn 6495  (class class class)co 7368   ↑_m cmap 8775

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-1st 7943  df-2nd 7944  df-map 8777

This theorem is referenced by:  mapxpen  9083  fsuppmapnn0fiublem  13925  fsuppmapnn0fiub  13926  fsuppmapnn0fiub0  13928  suppssfz  13929  fsuppmapnn0ub  13930  mndpsuppss  18702  mndpfsupp  18704  frlmbas  21722  frlmsslsp  21763  eqmat  22380  matplusgcell  22389  matsubgcell  22390  matvscacell  22392  cramerlem1  22643  tmdgsum  24051  fmptco1f1o  32722  islinds5  33459  ellspds  33460  1arithidomlem2  33628  1arithidom  33629  lbsdiflsp0  33803  matmpo  33980  1smat1  33981  actfunsnf1o  34781  actfunsnrndisj  34782  reprinfz1  34799  unccur  37851  matunitlindflem1  37864  matunitlindflem2  37865  poimirlem4  37872  poimirlem5  37873  poimirlem6  37874  poimirlem7  37875  poimirlem10  37878  poimirlem11  37879  poimirlem12  37880  poimirlem16  37884  poimirlem19  37887  poimirlem29  37897  poimirlem30  37898  poimirlem31  37899  broucube  37902  fsuppind  42945  ofoafo  43710  ofoaass  43714  ofoacom  43715  rfovcnvf1od  44357  dssmapnvod  44373  dssmapntrcls  44481  k0004lem3  44502  unirnmap  45563  unirnmapsn  45569  ssmapsn  45571  dvnprodlem1  46301  dvnprodlem3  46303  rrxsnicc  46655  ioorrnopnlem  46659  ovnsubaddlem1  46925  hoiqssbllem1  46977  iccpartrn  47787  iccpartf  47788  iccpartnel  47795  dflinc2  48767  lincsum  48786  lincresunit2  48835  2arymaptfo  49011  rrx2pnecoorneor  49072  rrx2linest  49099