Theorem elmapi 8793

Description: A mapping is a function, forward direction only with superfluous antecedent removed. (Contributed by Stefan O'Rear, 10-Oct-2014.)

Assertion

Ref	Expression
elmapi	⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → 𝐴:𝐶⟶𝐵)

Proof of Theorem elmapi

Step	Hyp	Ref	Expression
1		elmapex 8792	. . 3 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V))
2		elmapg 8783	. . 3 ⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝐴 ∈ (𝐵 ↑m 𝐶) ↔ 𝐴:𝐶⟶𝐵))
3	1, 2	syl 17	. 2 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → (𝐴 ∈ (𝐵 ↑m 𝐶) ↔ 𝐴:𝐶⟶𝐵))
4	3	ibi 268	1 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → 𝐴:𝐶⟶𝐵)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∈ wcel 2119  Vcvv 3432  ⟶wf 6488  (class class class)co 7363   ↑_m cmap 8770

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7366  df-oprab 7367  df-mpo 7368  df-1st 7938  df-2nd 7939  df-map 8772

This theorem is referenced by:  mapfset  8794  elmapfn  8809  elmapfun  8810  elmapssres  8811  mapsspm  8821  mapfvd  8824  elmapresaun  8825  map0b  8828  mapss  8834  mapsncnv  8838  ralxpmap  8841  mapen  9076  mapxpen  9078  mapunen  9081  mapfienlem1  9315  mapfienlem2  9316  mapfienlem3  9317  mapfien  9318  wemaplem2  9459  wemappo  9461  wemapsolem  9462  wemapso  9463  wemapso2lem  9464  wemapwe  9616  iunmapdisj  9943  fseqenlem1  9944  fseqenlem2  9945  numacn  9969  finacn  9970  acndom  9971  acndom2  9974  infpwfien  9982  infmap2  10137  fin23lem40  10271  isf32lem12  10284  isf34lem6  10300  acncc  10360  pwfseqlem3  10581  pwxpndom2  10586  ramval  16977  ramub  16982  ramcl  16998  prmgaplem7  17026  prmgaplem8  17027  imasdsval2  17478  funcf2  17833  funcpropd  17867  funcestrcsetclem8  18111  funcestrcsetclem9  18112  funcsetcestrclem8  18126  funcsetcestrclem9  18127  mndpsuppss  18731  mndvcl  18763  mndvass  18764  mndvlid  18765  mndvrid  18766  mhmvlin  18767  fsfnn0gsumfsffz  19956  gsummptnn0fzfv  19960  frlmfibas  21744  frlmbas3  21758  frlmipval  21761  frlmphllem  21762  frlmphl  21763  elfilspd  21785  islindf4  21820  psrbagf  21900  mplbas2  22025  ltbwe  22027  evlsvvvallem  22074  evlsvvval  22076  psr1baslem  22177  psr1basf  22193  fvcoe1  22199  coe1mul2lem1  22260  ply1coe  22291  mamures  22387  grpvlinv  22388  grpvrinv  22389  mamucl  22391  mamuass  22392  mamudi  22393  mamudir  22394  mamuvs1  22395  mamuvs2  22396  mamulid  22431  mamurid  22432  mattposcl  22443  mattpostpos  22444  tposmap  22447  mamutpos  22448  matgsumcl  22450  mavmulcl  22537  mavmulass  22539  mavmulsolcl  22541  marepvcl  22559  1marepvmarrepid  22565  mdetleib2  22578  mdetf  22585  mdetdiaglem  22588  mdetrlin  22592  mdetrsca  22593  mdetralt  22598  mdetunilem7  22608  mdetunilem9  22610  maducoeval2  22630  madutpos  22632  madugsum  22633  madurid  22634  cramerimplem1  22673  m2pmfzmap  22737  decpmatval  22755  pmatcollpw3lem  22773  pmatcollpw3fi1lem1  22776  pmatcollpw3fi1lem2  22777  pm2mp  22815  chfacfisf  22844  chfacfisfcpmat  22845  chfacfscmulgsum  22850  chfacfpmmulgsum  22854  chfacfpmmulgsum2  22855  cayhamlem1  22856  cpmadugsumlemF  22866  cpmadugsumfi  22867  cayhamlem2  22874  chcoeffeqlem  22875  cayleyhamilton1  22882  pnrmopn  23333  xkoptsub  23644  xkopt  23645  tmdgsum  24085  imasdsf1olem  24363  rrxnm  25383  rrxds  25385  rrxf  25393  rrxmvallem  25396  rrxbasefi  25402  rrxdsfi  25403  ehlbase  25407  ovolscalem2  25506  uniioombl  25581  tdeglem2  26051  plypf1  26202  ulmclm  26377  ulmcaulem  26384  ulmcau  26385  ulmss  26387  ulmbdd  26388  ulmcn  26389  ulmdvlem1  26390  ulmdvlem2  26391  ulmdvlem3  26392  mtest  26394  mtestbdd  26395  mbfulm  26396  iblulm  26397  itgulm  26398  itgulm2  26399  adjval2  31987  fmptco1f1o  32732  fcobijfs  32820  fcobijfs2  32821  resf1o  32829  fpwrelmap  32832  elrspunidl  33518  elrspunsn  33519  1arithidomlem2  33626  1arithidom  33627  fply1  33648  psrbasfsupp  33702  selvply1rhmlemb  33710  ply1degltdimlem  33813  fedgmullem1  33820  fedgmul  33822  extdg1id  33857  smatrcl  33987  mbfmf  34445  elmbfmvol2  34458  eulerpartlemelr  34548  eulerpartlemf  34561  eulerpartlemt  34562  eulerpartgbij  34563  eulerpartlemgu  34568  eulerpartlemgh  34569  eulerpartlemgf  34570  eulerpartlemgs2  34571  reprf  34803  reprsuc  34806  vtsprod  34830  circlemethhgt  34834  tgoldbachgtd  34853  satfv1lem  35597  satfvel  35647  satefvfmla0  35653  satefvfmla1  35660  prv1n  35666  mrsubff1  35749  mrsub0  35751  mrsubf  35752  mrsubccat  35753  mrsubcn  35754  msubrn  35764  msubff  35765  msubf  35767  msubff1  35791  mclsind  35805  uncf  37973  curunc  37976  unccur  37977  matunitlindflem1  37990  matunitlindflem2  37991  poimirlem4  37998  poimirlem5  37999  poimirlem6  38000  poimirlem7  38001  poimirlem8  38002  poimirlem10  38004  poimirlem11  38005  poimirlem12  38006  poimirlem16  38010  poimirlem17  38011  poimirlem18  38012  poimirlem19  38013  poimirlem20  38014  poimirlem21  38015  poimirlem22  38016  poimirlem25  38019  poimirlem26  38020  poimirlem27  38021  poimirlem29  38023  poimirlem30  38024  poimirlem31  38025  poimirlem32  38026  poimir  38027  broucube  38028  mblfinlem3  38033  mblfinlem4  38034  ismblfin  38035  rrnmet  38203  rrndstprj1  38204  rrndstprj2  38205  rrncmslem  38206  rrnequiv  38209  aks6d1c2lem4  42619  mapcod  42734  evlselv  43046  fsuppind  43047  mhphf  43054  mapco2g  43170  mapfzcons1  43173  mapfzcons2  43175  mzpcompact2lem  43207  eldiophb  43213  elmapresaunres2  43227  eq0rabdioph  43232  rexrabdioph  43246  eldioph4b  43263  diophren  43265  rmydioph  43466  rmxdioph  43468  expdiophlem2  43474  expdioph  43475  pw2f1o2val2  43492  wepwsolem  43494  pwfi2f1o  43548  ofoafo  43808  ofoaid1  43810  ofoaid2  43811  ofoaass  43812  ofoacom  43813  rfovcnvf1od  44455  rfovcnvfvd  44458  fsovrfovd  44460  fsovcnvlem  44464  ntrk0kbimka  44490  neik0pk1imk0  44498  ntrclsfveq1  44511  ntrclsfveq2  44512  ntrclsfveq  44513  ntrclsss  44514  ntrclsiso  44518  ntrclsk2  44519  ntrclskb  44520  ntrclsk3  44521  ntrclsk13  44522  ntrclsk4  44523  ntrneifv3  44533  ntrneineine0lem  44534  ntrneineine1lem  44535  ntrneifv4  44536  ntrneiel2  44537  ntrneicls00  44540  ntrneicls11  44541  ntrneiiso  44542  ntrneik2  44543  ntrneikb  44545  ntrneixb  44546  ntrneik3  44547  ntrneix3  44548  ntrneik13  44549  ntrneix13  44550  ntrneik4w  44551  ntrneik4  44552  clsneifv3  44561  clsneifv4  44562  neicvgfv  44572  k0004ss2  44603  k0004val0  44605  mnringbasefd  44669  mnugrud  44735  mapss2  45658  difmap  45659  inmap  45661  difmapsn  45664  ssmapsn  45668  mccllem  46049  dvnprodlem1  46396  dvnprodlem2  46397  fourierdlem11  46568  fourierdlem12  46569  fourierdlem13  46570  fourierdlem14  46571  fourierdlem34  46591  fourierdlem41  46598  fourierdlem48  46604  fourierdlem49  46605  fourierdlem54  46610  fourierdlem63  46619  fourierdlem64  46620  fourierdlem65  46621  fourierdlem69  46625  fourierdlem72  46628  fourierdlem74  46630  fourierdlem75  46631  fourierdlem79  46635  fourierdlem85  46641  fourierdlem88  46644  fourierdlem89  46645  fourierdlem90  46646  fourierdlem91  46647  fourierdlem92  46648  fourierdlem94  46650  fourierdlem97  46653  fourierdlem103  46659  fourierdlem104  46660  fourierdlem111  46667  fourierdlem113  46669  etransclem24  46708  etransclem26  46710  etransclem27  46711  etransclem28  46712  etransclem31  46715  etransclem32  46716  etransclem33  46717  etransclem34  46718  etransclem35  46719  etransclem37  46721  etransclem38  46722  rrxtopnfi  46737  rrndistlt  46740  qndenserrnbllem  46744  rrxsnicc  46750  ioorrnopnlem  46754  subsaliuncl  46808  hoicvr  46998  ovnprodcl  47004  ovnsupge0  47007  ovnlecvr  47008  ovncvrrp  47014  ovn0lem  47015  ovnsubaddlem1  47020  sge0hsphoire  47039  hoidmv1le  47044  hoidmvlelem1  47045  hoidmvlelem2  47046  hoidmvlelem3  47047  hoidmvlelem4  47048  hoidmvlelem5  47049  hoidmvle  47050  ovnhoilem2  47052  ovnlecvr2  47060  ovncvr2  47061  hoiqssbllem1  47072  hoiqssbllem2  47073  hoiqssbllem3  47074  hspmbllem2  47077  opnvonmbllem2  47083  ovolval2lem  47093  ovolval2  47094  ovolval3  47097  ovolval4lem2  47100  ovolval5lem3  47104  ovnovollem1  47106  ovnovollem2  47107  vonvolmbllem  47110  vonvolmbl2  47113  vonvol2  47114  snvonmbl  47136  vonsn  47141  iccpartxr  47901  nnsum4primeseven  48298  nnsum4primesevenALTV  48299  intop  48701  assintop  48707  isassintop  48708  ofaddmndmap  48841  rmsupp0  48866  domnmsuppn0  48867  rmsuppss  48868  scmsuppss  48869  gsumlsscl  48878  lincfsuppcl  48911  linccl  48912  lcosn0  48918  lincdifsn  48922  lincsum  48927  lincscm  48928  lincscmcl  48930  islinindfis  48947  lincext1  48952  lincext2  48953  lincext3  48954  lindslinindimp2lem1  48956  lindslinindimp2lem2  48957  lindslinindimp2lem4  48959  lindslinindsimp2lem5  48960  snlindsntor  48969  lincresunitlem2  48974  lincresunit3lem1  48977  lincresunit3lem2  48978  lincresunit3  48979  lincreslvec3  48980  isldepslvec2  48983  zlmodzxzldeplem2  48999  zlmodzxzldeplem3  49000  ldepsnlinclem1  49003  ldepsnlinclem2  49004  1arymaptf1  49140  1arymaptfo  49141  2arympt  49147  2arymaptf1  49151  2arymaptfo  49152  prelrrx2b  49212  eenglngeehlnmlem1  49235  eenglngeehlnmlem2  49236  aacllem  50298