Theorem elmapi 7879

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	⊢ (𝐴 ∈ (𝐵 ↑𝑚 𝐶) → 𝐴:𝐶⟶𝐵)

Proof of Theorem elmapi

Step	Hyp	Ref	Expression
1		elmapex 7878	. . 3 ⊢ (𝐴 ∈ (𝐵 ↑𝑚 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V))
2		elmapg 7870	. . 3 ⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝐴 ∈ (𝐵 ↑𝑚 𝐶) ↔ 𝐴:𝐶⟶𝐵))
3	1, 2	syl 17	. 2 ⊢ (𝐴 ∈ (𝐵 ↑𝑚 𝐶) → (𝐴 ∈ (𝐵 ↑𝑚 𝐶) ↔ 𝐴:𝐶⟶𝐵))
4	3	ibi 256	1 ⊢ (𝐴 ∈ (𝐵 ↑𝑚 𝐶) → 𝐴:𝐶⟶𝐵)

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∈ wcel 1990  Vcvv 3200  ⟶wf 5884  (class class class)co 6650   ↑_𝑚 cmap 7857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-1st 7168  df-2nd 7169  df-map 7859

This theorem is referenced by:  elmapfn  7880  elmapfun  7881  elmapssres  7882  mapsspm  7891  map0b  7896  mapss  7900  mapsncnv  7904  ralxpmap  7907  mapen  8124  mapxpen  8126  mapunen  8129  mapfienlem1  8310  mapfienlem2  8311  mapfienlem3  8312  mapfien  8313  wemaplem2  8452  wemappo  8454  wemapsolem  8455  wemapso  8456  wemapso2lem  8457  wemapwe  8594  iunmapdisj  8846  fseqenlem1  8847  fseqenlem2  8848  numacn  8872  finacn  8873  acndom  8874  acndom2  8877  infpwfien  8885  infmap2  9040  fin23lem40  9173  isf32lem12  9186  isf34lem6  9202  acncc  9262  pwfseqlem3  9482  pwxpndom2  9487  ramval  15712  ramub  15717  ramcl  15733  prmgaplem7  15761  prmgaplem8  15762  imasdsval2  16176  funcf2  16528  funcpropd  16560  funcestrcsetclem8  16787  funcestrcsetclem9  16788  funcsetcestrclem8  16802  funcsetcestrclem9  16803  fsfnn0gsumfsffz  18379  gsummptnn0fzfv  18384  mplbas2  19470  ltbwe  19472  psr1baslem  19555  psr1basf  19571  fvcoe1  19577  coe1mul2lem1  19637  ply1coe  19666  frlmfibas  20105  frlmbas3  20115  frlmipval  20118  frlmphllem  20119  frlmphl  20120  elfilspd  20142  islindf4  20177  mamures  20196  mndvcl  20197  mndvass  20198  mndvlid  20199  mndvrid  20200  grpvlinv  20201  grpvrinv  20202  mhmvlin  20203  mamucl  20207  mamuass  20208  mamudi  20209  mamudir  20210  mamuvs1  20211  mamuvs2  20212  mamulid  20247  mamurid  20248  mattposcl  20259  mattpostpos  20260  tposmap  20263  mamutpos  20264  matgsumcl  20266  mavmulcl  20353  mavmulass  20355  mavmulsolcl  20357  marepvcl  20375  1marepvmarrepid  20381  mdetleib2  20394  mdetf  20401  mdetdiaglem  20404  mdetrlin  20408  mdetrsca  20409  mdetralt  20414  mdetunilem7  20424  mdetunilem9  20426  maducoeval2  20446  madutpos  20448  madugsum  20449  madurid  20450  cramerimplem1  20489  m2pmfzmap  20552  decpmatval  20570  pmatcollpw3lem  20588  pmatcollpw3fi1lem1  20591  pmatcollpw3fi1lem2  20592  pm2mp  20630  chfacfisf  20659  chfacfisfcpmat  20660  chfacfscmulgsum  20665  chfacfpmmulgsum  20669  chfacfpmmulgsum2  20670  cayhamlem1  20671  cpmadugsumlemF  20681  cpmadugsumfi  20682  cayhamlem2  20689  chcoeffeqlem  20690  cayleyhamilton1  20697  pnrmopn  21147  xkoptsub  21457  xkopt  21458  tmdgsum  21899  imasdsf1olem  22178  rrxnm  23179  rrxds  23181  rrxf  23184  rrxmvallem  23187  ehlbase  23194  ovolscalem2  23282  uniioombl  23357  tdeglem2  23821  plypf1  23968  ulmclm  24141  ulmcaulem  24148  ulmcau  24149  ulmss  24151  ulmbdd  24152  ulmcn  24153  ulmdvlem1  24154  ulmdvlem2  24155  ulmdvlem3  24156  mtest  24158  mtestbdd  24159  mbfulm  24160  iblulm  24161  itgulm  24162  itgulm2  24163  adjval2  28750  fmptco1f1o  29434  fcobijfs  29501  resf1o  29505  fpwrelmap  29508  smatrcl  29862  mbfmf  30317  elmbfmvol2  30329  eulerpartlemelr  30419  eulerpartlemf  30432  eulerpartlemt  30433  eulerpartgbij  30434  eulerpartlemgu  30439  eulerpartlemgh  30440  eulerpartlemgf  30441  eulerpartlemgs2  30442  reprf  30690  reprsuc  30693  vtsprod  30717  circlemethhgt  30721  tgoldbachgtd  30740  mrsubff1  31411  mrsub0  31413  mrsubf  31414  mrsubccat  31415  mrsubcn  31416  msubrn  31426  msubff  31427  msubf  31429  msubff1  31453  mclsind  31467  uncf  33388  curunc  33391  unccur  33392  matunitlindflem1  33405  matunitlindflem2  33406  poimirlem4  33413  poimirlem5  33414  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem10  33419  poimirlem11  33420  poimirlem12  33421  poimirlem16  33425  poimirlem17  33426  poimirlem18  33427  poimirlem19  33428  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  poimirlem29  33438  poimirlem30  33439  poimirlem31  33440  poimirlem32  33441  poimir  33442  broucube  33443  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  rrnmet  33628  rrndstprj1  33629  rrndstprj2  33630  rrncmslem  33631  rrnequiv  33634  mapco2g  37277  mapfzcons1  37280  mapfzcons2  37282  mzpcompact2lem  37314  eldiophb  37320  elmapresaun  37334  elmapresaunres2  37335  eq0rabdioph  37340  rexrabdioph  37358  eldioph4b  37375  diophren  37377  rmydioph  37581  rmxdioph  37583  expdiophlem2  37589  expdioph  37590  pw2f1o2val2  37607  wepwsolem  37612  pwfi2f1o  37666  rfovcnvf1od  38298  rfovcnvfvd  38301  fsovrfovd  38303  fsovcnvlem  38307  ntrk0kbimka  38337  neik0pk1imk0  38345  ntrclsfveq1  38358  ntrclsfveq2  38359  ntrclsfveq  38360  ntrclsss  38361  ntrclsiso  38365  ntrclsk2  38366  ntrclskb  38367  ntrclsk3  38368  ntrclsk13  38369  ntrclsk4  38370  ntrneifv3  38380  ntrneineine0lem  38381  ntrneineine1lem  38382  ntrneifv4  38383  ntrneiel2  38384  ntrneicls00  38387  ntrneicls11  38388  ntrneiiso  38389  ntrneik2  38390  ntrneikb  38392  ntrneixb  38393  ntrneik3  38394  ntrneix3  38395  ntrneik13  38396  ntrneix13  38397  ntrneik4w  38398  ntrneik4  38399  clsneifv3  38408  clsneifv4  38409  neicvgfv  38419  k0004ss2  38450  k0004val0  38452  mapss2  39397  difmap  39399  inmap  39401  difmapsn  39404  ssmapsn  39408  mccllem  39829  dvnprodlem1  40161  dvnprodlem2  40162  fourierdlem11  40335  fourierdlem12  40336  fourierdlem13  40337  fourierdlem14  40338  fourierdlem34  40358  fourierdlem41  40365  fourierdlem48  40371  fourierdlem49  40372  fourierdlem54  40377  fourierdlem63  40386  fourierdlem64  40387  fourierdlem65  40388  fourierdlem69  40392  fourierdlem72  40395  fourierdlem74  40397  fourierdlem75  40398  fourierdlem79  40402  fourierdlem85  40408  fourierdlem88  40411  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem92  40415  fourierdlem94  40417  fourierdlem97  40420  fourierdlem103  40426  fourierdlem104  40427  fourierdlem111  40434  fourierdlem113  40436  etransclem24  40475  etransclem26  40477  etransclem27  40478  etransclem28  40479  etransclem31  40482  etransclem32  40483  etransclem33  40484  etransclem34  40485  etransclem35  40486  etransclem37  40488  etransclem38  40489  rrxbasefi  40503  rrxdsfi  40505  rrxtopnfi  40506  rrndistlt  40510  qndenserrnbllem  40514  rrxsnicc  40520  ioorrnopnlem  40524  subsaliuncl  40576  hoicvr  40762  ovnprodcl  40768  ovnsupge0  40771  ovnlecvr  40772  ovncvrrp  40778  ovn0lem  40779  ovnsubaddlem1  40784  sge0hsphoire  40803  hoidmv1le  40808  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvlelem4  40812  hoidmvlelem5  40813  hoidmvle  40814  ovnhoilem2  40816  ovnlecvr2  40824  ovncvr2  40825  hoiqssbllem1  40836  hoiqssbllem2  40837  hoiqssbllem3  40838  hspmbllem2  40841  opnvonmbllem2  40847  ovolval2lem  40857  ovolval2  40858  ovolval3  40861  ovolval4lem2  40864  ovolval5lem3  40868  ovnovollem1  40870  ovnovollem2  40871  vonvolmbllem  40874  vonvolmbl2  40877  vonvol2  40878  snvonmbl  40900  vonsn  40905  iccpartxr  41355  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  intop  41839  assintop  41845  isassintop  41846  ofaddmndmap  42122  rmsupp0  42149  domnmsuppn0  42150  rmsuppss  42151  mndpsuppss  42152  scmsuppss  42153  gsumlsscl  42164  lincfsuppcl  42202  linccl  42203  lcosn0  42209  lincdifsn  42213  lincsum  42218  lincscm  42219  lincscmcl  42221  islinindfis  42238  lincext1  42243  lincext2  42244  lincext3  42245  lindslinindimp2lem1  42247  lindslinindimp2lem2  42248  lindslinindimp2lem4  42250  lindslinindsimp2lem5  42251  snlindsntor  42260  lincresunitlem2  42265  lincresunit3lem1  42268  lincresunit3lem2  42269  lincresunit3  42270  lincreslvec3  42271  isldepslvec2  42274  zlmodzxzldeplem2  42290  zlmodzxzldeplem3  42291  ldepsnlinclem1  42294  ldepsnlinclem2  42295  aacllem  42547