Theorem elmapi 8897

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2147  Vcvv 3454  ⟶wf 6554  (class class class)co 7443   ↑_m cmap 8875

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-fv 6566  df-ov 7446  df-oprab 7447  df-mpo 7448  df-1st 8025  df-2nd 8026  df-map 8877

This theorem is used by:  elmaprd  8898  mapfset  8900  elmapfn  8915  elmapfun  8916  uncf  8919  elmapssres  8922  mapsspm  8932  mapfvd  8935  elmapresaun  8936  map0b  8939  mapss  8945  mapsncnv  8949  ralxpmap  8952  mapen  9188  mapxpen  9190  mapunen  9193  mapfienlem1  9424  mapfienlem2  9425  mapfienlem3  9426  mapfien  9427  wemaplem2  9568  wemappo  9570  wemapsolem  9571  wemapso  9572  wemapso2lem  9573  wemapwe  9725  iunmapdisj  10129  fseqenlem1  10130  fseqenlem2  10131  numacn  10155  finacn  10156  acndom  10157  acndom2  10160  infpwfien  10168  infmap2  10322  fin23lem40  10456  isf32lem12  10469  isf34lem6  10485  acncc  10545  pwfseqlem3  10772  pwxpndom2  10777  s3rex  15130  ramval  17215  ramub  17220  ramcl  17236  prmgaplem7  17264  prmgaplem8  17265  imasdsval2  17717  funcf2  18072  funcpropd  18106  funcestrcsetclem8  18350  funcestrcsetclem9  18351  funcsetcestrclem8  18365  funcsetcestrclem9  18366  mndpsuppss  18988  mndvcl  19021  mndvass  19022  mndvlid  19023  mndvrid  19024  mhmvlin  19025  fsfnn0gsumfsffz  20227  gsummptnn0fzfv  20231  frlmfibas  22098  frlmbas3  22112  frlmipval  22115  frlmphllem  22116  frlmphl  22117  elfilspd  22139  islindf4  22174  psrbagf  22256  mplbas2  22381  ltbwe  22383  evlsvvvallem  22430  evlsvvval  22432  psr1baslem  22533  psr1basf  22549  fvcoe1  22555  coe1mul2lem1  22616  ply1coe  22646  mamures  22742  grpvlinv  22743  grpvrinv  22744  mamucl  22746  mamuass  22747  mamudi  22748  mamudir  22749  mamuvs1  22750  mamuvs2  22751  mamulid  22786  mamurid  22787  mattposcl  22798  mattpostpos  22799  tposmap  22802  mamutpos  22803  matgsumcl  22805  mavmulcl  22892  mavmulass  22894  mavmulsolcl  22896  marepvcl  22914  1marepvmarrepid  22920  mdetleib2  22933  mdetf  22940  mdetdiaglem  22943  mdetrlin  22947  mdetrsca  22948  mdetralt  22953  mdetunilem7  22963  mdetunilem9  22965  maducoeval2  22985  madutpos  22987  madugsum  22988  madurid  22989  matunitlindflem1  23024  matunitlindflem2  23025  cramerimplem1  23031  m2pmfzmap  23095  decpmatval  23113  pmatcollpw3lem  23131  pmatcollpw3fi1lem1  23134  pmatcollpw3fi1lem2  23135  pm2mp  23173  chfacfisf  23202  chfacfisfcpmat  23203  chfacfscmulgsum  23208  chfacfpmmulgsum  23212  chfacfpmmulgsum2  23213  cayhamlem1  23214  cpmadugsumlemF  23224  cpmadugsumfi  23225  cayhamlem2  23232  chcoeffeqlem  23233  cayleyhamilton1  23240  pnrmopn  23691  xkoptsub  24003  xkopt  24004  tmdgsum  24444  imasdsf1olem  24722  rrxnm  25742  rrxds  25744  rrxf  25752  rrxmvallem  25755  rrxbasefi  25761  rrxdsfi  25762  ehlbase  25766  ovolscalem2  25865  uniioombl  25940  tdeglem2  26409  plypf1  26561  ulmclm  26744  ulmcaulem  26751  ulmcau  26752  ulmss  26754  ulmbdd  26755  ulmcn  26756  ulmdvlem1  26757  ulmdvlem2  26758  ulmdvlem3  26759  mtest  26761  mtestbdd  26762  mbfulm  26763  iblulm  26764  itgulm  26765  itgulm2  26766  adjval2  32523  fmptco1f1o  33299  fcobijfs  33383  fcobijfs2  33384  resf1o  33392  fpwrelmap  33395  elrspunidl  34048  elrspunsn  34049  1arithidomlem2  34138  1arithidom  34139  fply1  34160  psrbasfsupp  34213  selvply1rhmlemb  34221  ply1degltdimlem  34324  fedgmullem1  34331  fedgmul  34333  extdg1id  34368  smatrcl  34498  mbfmf  34957  elmbfmvol2  34969  eulerpartlemelr  35059  eulerpartlemf  35072  eulerpartlemt  35073  eulerpartgbij  35074  eulerpartlemgu  35079  eulerpartlemgh  35080  eulerpartlemgf  35081  eulerpartlemgs2  35082  reprf  35311  reprsuc  35314  vtsprod  35338  circlemethhgt  35342  tgoldbachgtd  35361  satfv1lem  36294  satfvel  36344  satefvfmla0  36350  satefvfmla1  36357  prv1n  36363  mrsubff1  36446  mrsub0  36448  mrsubf  36449  mrsubccat  36450  mrsubcn  36451  msubrn  36461  msubff  36462  msubf  36464  msubff1  36488  mclsind  36502  curunc  38717  unccur  38718  poimirlem4  38734  poimirlem5  38735  poimirlem6  38736  poimirlem7  38737  poimirlem8  38738  poimirlem10  38740  poimirlem11  38741  poimirlem12  38742  poimirlem16  38746  poimirlem17  38747  poimirlem18  38748  poimirlem19  38749  poimirlem20  38750  poimirlem21  38751  poimirlem22  38752  poimirlem25  38755  poimirlem26  38756  poimirlem27  38757  poimirlem29  38759  poimirlem30  38760  poimirlem31  38761  poimirlem32  38762  poimir  38763  broucube  38764  mblfinlem3  38769  mblfinlem4  38770  ismblfin  38771  rrnmet  38955  rrndstprj1  38956  rrndstprj2  38957  rrncmslem  38958  rrnequiv  38961  aks6d1c2lem4  43369  mapcod  43487  evlselv  43810  fsuppind  43811  mhphf  43818  mapco2g  43918  mapfzcons1  43921  mapfzcons2  43923  mzpcompact2lem  43955  eldiophb  43961  elmapresaunres2  43975  eq0rabdioph  43980  rexrabdioph  43994  eldioph4b  44011  diophren  44013  rmydioph  44214  rmxdioph  44216  expdiophlem2  44222  expdioph  44223  pw2f1o2val2  44240  wepwsolem  44242  pwfi2f1o  44291  ofoafo  44550  ofoaid1  44552  ofoaid2  44553  ofoaass  44554  ofoacom  44555  rfovcnvf1od  45196  rfovcnvfvd  45199  fsovrfovd  45201  fsovcnvlem  45205  ntrk0kbimka  45231  neik0pk1imk0  45239  ntrclsfveq1  45252  ntrclsfveq2  45253  ntrclsfveq  45254  ntrclsss  45255  ntrclsiso  45259  ntrclsk2  45260  ntrclskb  45261  ntrclsk3  45262  ntrclsk13  45263  ntrclsk4  45264  ntrneifv3  45274  ntrneineine0lem  45275  ntrneineine1lem  45276  ntrneifv4  45277  ntrneiel2  45278  ntrneicls00  45281  ntrneicls11  45282  ntrneiiso  45283  ntrneik2  45284  ntrneikb  45286  ntrneixb  45287  ntrneik3  45288  ntrneix3  45289  ntrneik13  45290  ntrneix13  45291  ntrneik4w  45292  ntrneik4  45293  clsneifv3  45302  clsneifv4  45303  neicvgfv  45313  k0004ss2  45344  k0004val0  45346  mnringbasefd  45408  mnugrud  45460  mapss2  46424  difmap  46425  inmap  46427  difmapsn  46430  ssmapsn  46434  mccllem  46814  dvnprodlem1  47161  dvnprodlem2  47162  fourierdlem11  47333  fourierdlem12  47334  fourierdlem13  47335  fourierdlem14  47336  fourierdlem34  47356  fourierdlem41  47363  fourierdlem48  47369  fourierdlem49  47370  fourierdlem54  47375  fourierdlem63  47384  fourierdlem64  47385  fourierdlem65  47386  fourierdlem69  47390  fourierdlem72  47393  fourierdlem74  47395  fourierdlem75  47396  fourierdlem79  47400  fourierdlem85  47406  fourierdlem88  47409  fourierdlem89  47410  fourierdlem90  47411  fourierdlem91  47412  fourierdlem92  47413  fourierdlem94  47415  fourierdlem97  47418  fourierdlem103  47424  fourierdlem104  47425  fourierdlem111  47432  fourierdlem113  47434  etransclem24  47473  etransclem26  47475  etransclem27  47476  etransclem28  47477  etransclem31  47480  etransclem32  47481  etransclem33  47482  etransclem34  47483  etransclem35  47484  etransclem37  47486  etransclem38  47487  rrxtopnfi  47502  rrndistlt  47505  qndenserrnbllem  47509  rrxsnicc  47515  ioorrnopnlem  47519  subsaliuncl  47573  hoicvr  47763  ovnprodcl  47769  ovnsupge0  47772  ovnlecvr  47773  ovncvrrp  47779  ovn0lem  47780  ovnsubaddlem1  47785  sge0hsphoire  47804  hoidmv1le  47809  hoidmvlelem1  47810  hoidmvlelem2  47811  hoidmvlelem3  47812  hoidmvlelem4  47813  hoidmvlelem5  47814  hoidmvle  47815  ovnhoilem2  47817  ovnlecvr2  47825  ovncvr2  47826  hoiqssbllem1  47837  hoiqssbllem2  47838  hoiqssbllem3  47839  hspmbllem2  47842  opnvonmbllem2  47848  ovolval2lem  47858  ovolval2  47859  ovolval3  47862  ovolval4lem2  47865  ovolval5lem3  47869  ovnovollem1  47871  ovnovollem2  47872  vonvolmbllem  47875  vonvolmbl2  47878  vonvol2  47879  snvonmbl  47901  vonsn  47906  tmachlem-agreeprod  48152  tmachlem-tpopen  48156  iccpartxr  48706  nnsum4primeseven  49103  nnsum4primesevenALTV  49104  intop  49505  assintop  49511  isassintop  49512  ofaddmndmap  49660  rmsupp0  49685  domnmsuppn0  49686  rmsuppss  49687  scmsuppss  49688  gsumlsscl  49697  lincfsuppcl  49730  linccl  49731  lcosn0  49737  lincdifsn  49741  lincsum  49746  lincscm  49747  lincscmcl  49749  islinindfis  49766  lincext1  49771  lincext2  49772  lincext3  49773  lindslinindimp2lem1  49775  lindslinindimp2lem2  49776  lindslinindimp2lem4  49778  lindslinindsimp2lem5  49779  snlindsntor  49788  lincresunitlem2  49793  lincresunit3lem1  49796  lincresunit3lem2  49797  lincresunit3  49798  lincreslvec3  49799  isldepslvec2  49802  zlmodzxzldeplem2  49818  zlmodzxzldeplem3  49819  ldepsnlinclem1  49822  ldepsnlinclem2  49823  1arymaptf1  49959  1arymaptfo  49960  2arympt  49966  2arymaptf1  49970  2arymaptfo  49971  eenglngeehlnmlem1  50055  eenglngeehlnmlem2  50056  aacllem  51219  rr3fvcl  51226  crosspdotsumlem  51244  crossp3d  51247