Theorem elmapi 8889

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 8888	. . 3 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V))
2		elmapg 8879	. . 3 ⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝐴 ∈ (𝐵 ↑m 𝐶) ↔ 𝐴:𝐶⟶𝐵))
3	1, 2	syl 17	. 2 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → (𝐴 ∈ (𝐵 ↑m 𝐶) ↔ 𝐴:𝐶⟶𝐵))
4	3	ibi 267	1 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → 𝐴:𝐶⟶𝐵)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  Vcvv 3480  ⟶wf 6557  (class class class)co 7431   ↑_m cmap 8866

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8014  df-2nd 8015  df-map 8868

This theorem is referenced by:  mapfset  8890  elmapfn  8905  elmapfun  8906  elmapssres  8907  mapsspm  8916  mapfvd  8919  elmapresaun  8920  map0b  8923  mapss  8929  mapsncnv  8933  ralxpmap  8936  mapen  9181  mapxpen  9183  mapunen  9186  mapfienlem1  9445  mapfienlem2  9446  mapfienlem3  9447  mapfien  9448  wemaplem2  9587  wemappo  9589  wemapsolem  9590  wemapso  9591  wemapso2lem  9592  wemapwe  9737  iunmapdisj  10063  fseqenlem1  10064  fseqenlem2  10065  numacn  10089  finacn  10090  acndom  10091  acndom2  10094  infpwfien  10102  infmap2  10257  fin23lem40  10391  isf32lem12  10404  isf34lem6  10420  acncc  10480  pwfseqlem3  10700  pwxpndom2  10705  ramval  17046  ramub  17051  ramcl  17067  prmgaplem7  17095  prmgaplem8  17096  imasdsval2  17561  funcf2  17913  funcpropd  17947  funcestrcsetclem8  18192  funcestrcsetclem9  18193  funcsetcestrclem8  18207  funcsetcestrclem9  18208  mndpsuppss  18778  mndvcl  18810  mndvass  18811  mndvlid  18812  mndvrid  18813  mhmvlin  18814  fsfnn0gsumfsffz  20001  gsummptnn0fzfv  20005  frlmfibas  21782  frlmbas3  21796  frlmipval  21799  frlmphllem  21800  frlmphl  21801  elfilspd  21823  islindf4  21858  psrbagf  21938  mplbas2  22060  ltbwe  22062  psr1baslem  22186  psr1basf  22203  fvcoe1  22209  coe1mul2lem1  22270  ply1coe  22302  mamures  22401  grpvlinv  22402  grpvrinv  22403  mamucl  22405  mamuass  22406  mamudi  22407  mamudir  22408  mamuvs1  22409  mamuvs2  22410  mamulid  22447  mamurid  22448  mattposcl  22459  mattpostpos  22460  tposmap  22463  mamutpos  22464  matgsumcl  22466  mavmulcl  22553  mavmulass  22555  mavmulsolcl  22557  marepvcl  22575  1marepvmarrepid  22581  mdetleib2  22594  mdetf  22601  mdetdiaglem  22604  mdetrlin  22608  mdetrsca  22609  mdetralt  22614  mdetunilem7  22624  mdetunilem9  22626  maducoeval2  22646  madutpos  22648  madugsum  22649  madurid  22650  cramerimplem1  22689  m2pmfzmap  22753  decpmatval  22771  pmatcollpw3lem  22789  pmatcollpw3fi1lem1  22792  pmatcollpw3fi1lem2  22793  pm2mp  22831  chfacfisf  22860  chfacfisfcpmat  22861  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  chfacfpmmulgsum2  22871  cayhamlem1  22872  cpmadugsumlemF  22882  cpmadugsumfi  22883  cayhamlem2  22890  chcoeffeqlem  22891  cayleyhamilton1  22898  pnrmopn  23351  xkoptsub  23662  xkopt  23663  tmdgsum  24103  imasdsf1olem  24383  rrxnm  25425  rrxds  25427  rrxf  25435  rrxmvallem  25438  rrxbasefi  25444  rrxdsfi  25445  ehlbase  25449  ovolscalem2  25549  uniioombl  25624  tdeglem2  26100  plypf1  26251  ulmclm  26430  ulmcaulem  26437  ulmcau  26438  ulmss  26440  ulmbdd  26441  ulmcn  26442  ulmdvlem1  26443  ulmdvlem2  26444  ulmdvlem3  26445  mtest  26447  mtestbdd  26448  mbfulm  26449  iblulm  26450  itgulm  26451  itgulm2  26452  adjval2  31910  fmptco1f1o  32643  fcobijfs  32734  resf1o  32741  fpwrelmap  32744  elrspunidl  33456  elrspunsn  33457  1arithidomlem2  33564  1arithidom  33565  fply1  33584  ply1degltdimlem  33673  fedgmullem1  33680  fedgmul  33682  extdg1id  33716  smatrcl  33795  mbfmf  34255  elmbfmvol2  34269  eulerpartlemelr  34359  eulerpartlemf  34372  eulerpartlemt  34373  eulerpartgbij  34374  eulerpartlemgu  34379  eulerpartlemgh  34380  eulerpartlemgf  34381  eulerpartlemgs2  34382  reprf  34627  reprsuc  34630  vtsprod  34654  circlemethhgt  34658  tgoldbachgtd  34677  satfv1lem  35367  satfvel  35417  satefvfmla0  35423  satefvfmla1  35430  prv1n  35436  mrsubff1  35519  mrsub0  35521  mrsubf  35522  mrsubccat  35523  mrsubcn  35524  msubrn  35534  msubff  35535  msubf  35537  msubff1  35561  mclsind  35575  uncf  37606  curunc  37609  unccur  37610  matunitlindflem1  37623  matunitlindflem2  37624  poimirlem4  37631  poimirlem5  37632  poimirlem6  37633  poimirlem7  37634  poimirlem8  37635  poimirlem10  37637  poimirlem11  37638  poimirlem12  37639  poimirlem16  37643  poimirlem17  37644  poimirlem18  37645  poimirlem19  37646  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  poimirlem29  37656  poimirlem30  37657  poimirlem31  37658  poimirlem32  37659  poimir  37660  broucube  37661  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  rrnmet  37836  rrndstprj1  37837  rrndstprj2  37838  rrncmslem  37839  rrnequiv  37842  aks6d1c2lem4  42128  mapcod  42284  evlsvvvallem  42571  evlsvvval  42573  evlselv  42597  fsuppind  42600  mhphf  42607  mapco2g  42725  mapfzcons1  42728  mapfzcons2  42730  mzpcompact2lem  42762  eldiophb  42768  elmapresaunres2  42782  eq0rabdioph  42787  rexrabdioph  42805  eldioph4b  42822  diophren  42824  rmydioph  43026  rmxdioph  43028  expdiophlem2  43034  expdioph  43035  pw2f1o2val2  43052  wepwsolem  43054  pwfi2f1o  43108  ofoafo  43369  ofoaid1  43371  ofoaid2  43372  ofoaass  43373  ofoacom  43374  rfovcnvf1od  44017  rfovcnvfvd  44020  fsovrfovd  44022  fsovcnvlem  44026  ntrk0kbimka  44052  neik0pk1imk0  44060  ntrclsfveq1  44073  ntrclsfveq2  44074  ntrclsfveq  44075  ntrclsss  44076  ntrclsiso  44080  ntrclsk2  44081  ntrclskb  44082  ntrclsk3  44083  ntrclsk13  44084  ntrclsk4  44085  ntrneifv3  44095  ntrneineine0lem  44096  ntrneineine1lem  44097  ntrneifv4  44098  ntrneiel2  44099  ntrneicls00  44102  ntrneicls11  44103  ntrneiiso  44104  ntrneik2  44105  ntrneikb  44107  ntrneixb  44108  ntrneik3  44109  ntrneix3  44110  ntrneik13  44111  ntrneix13  44112  ntrneik4w  44113  ntrneik4  44114  clsneifv3  44123  clsneifv4  44124  neicvgfv  44134  k0004ss2  44165  k0004val0  44167  mnringbasefd  44234  mnugrud  44303  mapss2  45210  difmap  45212  inmap  45214  difmapsn  45217  ssmapsn  45221  mccllem  45612  dvnprodlem1  45961  dvnprodlem2  45962  fourierdlem11  46133  fourierdlem12  46134  fourierdlem13  46135  fourierdlem14  46136  fourierdlem34  46156  fourierdlem41  46163  fourierdlem48  46169  fourierdlem49  46170  fourierdlem54  46175  fourierdlem63  46184  fourierdlem64  46185  fourierdlem65  46186  fourierdlem69  46190  fourierdlem72  46193  fourierdlem74  46195  fourierdlem75  46196  fourierdlem79  46200  fourierdlem85  46206  fourierdlem88  46209  fourierdlem89  46210  fourierdlem90  46211  fourierdlem91  46212  fourierdlem92  46213  fourierdlem94  46215  fourierdlem97  46218  fourierdlem103  46224  fourierdlem104  46225  fourierdlem111  46232  fourierdlem113  46234  etransclem24  46273  etransclem26  46275  etransclem27  46276  etransclem28  46277  etransclem31  46280  etransclem32  46281  etransclem33  46282  etransclem34  46283  etransclem35  46284  etransclem37  46286  etransclem38  46287  rrxtopnfi  46302  rrndistlt  46305  qndenserrnbllem  46309  rrxsnicc  46315  ioorrnopnlem  46319  subsaliuncl  46373  hoicvr  46563  ovnprodcl  46569  ovnsupge0  46572  ovnlecvr  46573  ovncvrrp  46579  ovn0lem  46580  ovnsubaddlem1  46585  sge0hsphoire  46604  hoidmv1le  46609  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvlelem4  46613  hoidmvlelem5  46614  hoidmvle  46615  ovnhoilem2  46617  ovnlecvr2  46625  ovncvr2  46626  hoiqssbllem1  46637  hoiqssbllem2  46638  hoiqssbllem3  46639  hspmbllem2  46642  opnvonmbllem2  46648  ovolval2lem  46658  ovolval2  46659  ovolval3  46662  ovolval4lem2  46665  ovolval5lem3  46669  ovnovollem1  46671  ovnovollem2  46672  vonvolmbllem  46675  vonvolmbl2  46678  vonvol2  46679  snvonmbl  46701  vonsn  46706  iccpartxr  47406  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  intop  48119  assintop  48125  isassintop  48126  ofaddmndmap  48259  rmsupp0  48284  domnmsuppn0  48285  rmsuppss  48286  scmsuppss  48287  gsumlsscl  48296  lincfsuppcl  48330  linccl  48331  lcosn0  48337  lincdifsn  48341  lincsum  48346  lincscm  48347  lincscmcl  48349  islinindfis  48366  lincext1  48371  lincext2  48372  lincext3  48373  lindslinindimp2lem1  48375  lindslinindimp2lem2  48376  lindslinindimp2lem4  48378  lindslinindsimp2lem5  48379  snlindsntor  48388  lincresunitlem2  48393  lincresunit3lem1  48396  lincresunit3lem2  48397  lincresunit3  48398  lincreslvec3  48399  isldepslvec2  48402  zlmodzxzldeplem2  48418  zlmodzxzldeplem3  48419  ldepsnlinclem1  48422  ldepsnlinclem2  48423  1arymaptf1  48563  1arymaptfo  48564  2arympt  48570  2arymaptf1  48574  2arymaptfo  48575  prelrrx2b  48635  eenglngeehlnmlem1  48658  eenglngeehlnmlem2  48659  aacllem  49320