Theorem elmapfn 8850

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

Syntax hints:   → wi 4   ∈ wcel 2145   Fn wfn 6520  (class class class)co 7400   ↑_m cmap 8812

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pow 5326  ax-pr 5394  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5105  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-fv 6533  df-ov 7403  df-oprab 7404  df-mpo 7405  df-1st 7974  df-2nd 7975  df-map 8814

This theorem is referenced by:  mapxpen  9119  fsuppmapnn0fiublem  14014  fsuppmapnn0fiub  14015  fsuppmapnn0fiub0  14017  suppssfz  14018  fsuppmapnn0ub  14019  mndpsuppss  18811  mndpfsupp  18813  frlmbas  21862  frlmsslsp  21903  eqmat  22538  matplusgcell  22547  matsubgcell  22548  matvscacell  22550  cramerlem1  22801  tmdgsum  24209  fmptco1f1o  32886  islinds5  33592  ellspds  33593  1arithidomlem2  33738  1arithidom  33739  selvply1rhmlemb  33821  lbsdiflsp0  33928  matmpo  34105  1smat1  34106  actfunsnf1o  34903  actfunsnrndisj  34904  reprinfz1  34921  unccur  38109  matunitlindflem1  38122  matunitlindflem2  38123  poimirlem4  38130  poimirlem5  38131  poimirlem6  38132  poimirlem7  38133  poimirlem10  38136  poimirlem11  38137  poimirlem12  38138  poimirlem16  38142  poimirlem19  38145  poimirlem29  38155  poimirlem30  38156  poimirlem31  38157  broucube  38160  fsuppind  43179  ofoafo  43940  ofoaass  43944  ofoacom  43945  rfovcnvf1od  44587  dssmapnvod  44603  dssmapntrcls  44711  k0004lem3  44732  unirnmap  45783  unirnmapsn  45789  ssmapsn  45791  dvnprodlem1  46519  dvnprodlem3  46521  rrxsnicc  46873  ioorrnopnlem  46877  ovnsubaddlem1  47143  hoiqssbllem1  47195  iccpartrn  48035  iccpartf  48036  iccpartnel  48043  dflinc2  49042  lincsum  49061  lincresunit2  49110  2arymaptfo  49286  rrx2pnecoorneor  49347  rrx2linest  49374