Theorem elmapi 8779

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 8778	. . 3 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V))
2		elmapg 8769	. . 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 2113  Vcvv 3437  ⟶wf 6482  (class class class)co 7352   ↑_m cmap 8756

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-fv 6494  df-ov 7355  df-oprab 7356  df-mpo 7357  df-1st 7927  df-2nd 7928  df-map 8758

This theorem is referenced by:  mapfset  8780  elmapfn  8795  elmapfun  8796  elmapssres  8797  mapsspm  8806  mapfvd  8809  elmapresaun  8810  map0b  8813  mapss  8819  mapsncnv  8823  ralxpmap  8826  mapen  9061  mapxpen  9063  mapunen  9066  mapfienlem1  9296  mapfienlem2  9297  mapfienlem3  9298  mapfien  9299  wemaplem2  9440  wemappo  9442  wemapsolem  9443  wemapso  9444  wemapso2lem  9445  wemapwe  9594  iunmapdisj  9921  fseqenlem1  9922  fseqenlem2  9923  numacn  9947  finacn  9948  acndom  9949  acndom2  9952  infpwfien  9960  infmap2  10115  fin23lem40  10249  isf32lem12  10262  isf34lem6  10278  acncc  10338  pwfseqlem3  10558  pwxpndom2  10563  ramval  16922  ramub  16927  ramcl  16943  prmgaplem7  16971  prmgaplem8  16972  imasdsval2  17422  funcf2  17777  funcpropd  17811  funcestrcsetclem8  18055  funcestrcsetclem9  18056  funcsetcestrclem8  18070  funcsetcestrclem9  18071  mndpsuppss  18675  mndvcl  18707  mndvass  18708  mndvlid  18709  mndvrid  18710  mhmvlin  18711  fsfnn0gsumfsffz  19897  gsummptnn0fzfv  19901  frlmfibas  21701  frlmbas3  21715  frlmipval  21718  frlmphllem  21719  frlmphl  21720  elfilspd  21742  islindf4  21777  psrbagf  21857  mplbas2  21978  ltbwe  21980  psr1baslem  22098  psr1basf  22115  fvcoe1  22121  coe1mul2lem1  22182  ply1coe  22214  mamures  22313  grpvlinv  22314  grpvrinv  22315  mamucl  22317  mamuass  22318  mamudi  22319  mamudir  22320  mamuvs1  22321  mamuvs2  22322  mamulid  22357  mamurid  22358  mattposcl  22369  mattpostpos  22370  tposmap  22373  mamutpos  22374  matgsumcl  22376  mavmulcl  22463  mavmulass  22465  mavmulsolcl  22467  marepvcl  22485  1marepvmarrepid  22491  mdetleib2  22504  mdetf  22511  mdetdiaglem  22514  mdetrlin  22518  mdetrsca  22519  mdetralt  22524  mdetunilem7  22534  mdetunilem9  22536  maducoeval2  22556  madutpos  22558  madugsum  22559  madurid  22560  cramerimplem1  22599  m2pmfzmap  22663  decpmatval  22681  pmatcollpw3lem  22699  pmatcollpw3fi1lem1  22702  pmatcollpw3fi1lem2  22703  pm2mp  22741  chfacfisf  22770  chfacfisfcpmat  22771  chfacfscmulgsum  22776  chfacfpmmulgsum  22780  chfacfpmmulgsum2  22781  cayhamlem1  22782  cpmadugsumlemF  22792  cpmadugsumfi  22793  cayhamlem2  22800  chcoeffeqlem  22801  cayleyhamilton1  22808  pnrmopn  23259  xkoptsub  23570  xkopt  23571  tmdgsum  24011  imasdsf1olem  24289  rrxnm  25319  rrxds  25321  rrxf  25329  rrxmvallem  25332  rrxbasefi  25338  rrxdsfi  25339  ehlbase  25343  ovolscalem2  25443  uniioombl  25518  tdeglem2  25994  plypf1  26145  ulmclm  26324  ulmcaulem  26331  ulmcau  26332  ulmss  26334  ulmbdd  26335  ulmcn  26336  ulmdvlem1  26337  ulmdvlem2  26338  ulmdvlem3  26339  mtest  26341  mtestbdd  26342  mbfulm  26343  iblulm  26344  itgulm  26345  itgulm2  26346  adjval2  31873  fmptco1f1o  32617  fcobijfs  32708  fcobijfs2  32709  resf1o  32717  fpwrelmap  32720  elrspunidl  33400  elrspunsn  33401  1arithidomlem2  33508  1arithidom  33509  fply1  33528  psrbasfsupp  33579  ply1degltdimlem  33656  fedgmullem1  33663  fedgmul  33665  extdg1id  33700  smatrcl  33830  mbfmf  34288  elmbfmvol2  34301  eulerpartlemelr  34391  eulerpartlemf  34404  eulerpartlemt  34405  eulerpartgbij  34406  eulerpartlemgu  34411  eulerpartlemgh  34412  eulerpartlemgf  34413  eulerpartlemgs2  34414  reprf  34646  reprsuc  34649  vtsprod  34673  circlemethhgt  34677  tgoldbachgtd  34696  satfv1lem  35427  satfvel  35477  satefvfmla0  35483  satefvfmla1  35490  prv1n  35496  mrsubff1  35579  mrsub0  35581  mrsubf  35582  mrsubccat  35583  mrsubcn  35584  msubrn  35594  msubff  35595  msubf  35597  msubff1  35621  mclsind  35635  uncf  37659  curunc  37662  unccur  37663  matunitlindflem1  37676  matunitlindflem2  37677  poimirlem4  37684  poimirlem5  37685  poimirlem6  37686  poimirlem7  37687  poimirlem8  37688  poimirlem10  37690  poimirlem11  37691  poimirlem12  37692  poimirlem16  37696  poimirlem17  37697  poimirlem18  37698  poimirlem19  37699  poimirlem20  37700  poimirlem21  37701  poimirlem22  37702  poimirlem25  37705  poimirlem26  37706  poimirlem27  37707  poimirlem29  37709  poimirlem30  37710  poimirlem31  37711  poimirlem32  37712  poimir  37713  broucube  37714  mblfinlem3  37719  mblfinlem4  37720  ismblfin  37721  rrnmet  37889  rrndstprj1  37890  rrndstprj2  37891  rrncmslem  37892  rrnequiv  37895  aks6d1c2lem4  42240  mapcod  42361  evlsvvvallem  42679  evlsvvval  42681  evlselv  42705  fsuppind  42708  mhphf  42715  mapco2g  42831  mapfzcons1  42834  mapfzcons2  42836  mzpcompact2lem  42868  eldiophb  42874  elmapresaunres2  42888  eq0rabdioph  42893  rexrabdioph  42911  eldioph4b  42928  diophren  42930  rmydioph  43131  rmxdioph  43133  expdiophlem2  43139  expdioph  43140  pw2f1o2val2  43157  wepwsolem  43159  pwfi2f1o  43213  ofoafo  43473  ofoaid1  43475  ofoaid2  43476  ofoaass  43477  ofoacom  43478  rfovcnvf1od  44121  rfovcnvfvd  44124  fsovrfovd  44126  fsovcnvlem  44130  ntrk0kbimka  44156  neik0pk1imk0  44164  ntrclsfveq1  44177  ntrclsfveq2  44178  ntrclsfveq  44179  ntrclsss  44180  ntrclsiso  44184  ntrclsk2  44185  ntrclskb  44186  ntrclsk3  44187  ntrclsk13  44188  ntrclsk4  44189  ntrneifv3  44199  ntrneineine0lem  44200  ntrneineine1lem  44201  ntrneifv4  44202  ntrneiel2  44203  ntrneicls00  44206  ntrneicls11  44207  ntrneiiso  44208  ntrneik2  44209  ntrneikb  44211  ntrneixb  44212  ntrneik3  44213  ntrneix3  44214  ntrneik13  44215  ntrneix13  44216  ntrneik4w  44217  ntrneik4  44218  clsneifv3  44227  clsneifv4  44228  neicvgfv  44238  k0004ss2  44269  k0004val0  44271  mnringbasefd  44335  mnugrud  44401  mapss2  45326  difmap  45328  inmap  45330  difmapsn  45333  ssmapsn  45337  mccllem  45721  dvnprodlem1  46068  dvnprodlem2  46069  fourierdlem11  46240  fourierdlem12  46241  fourierdlem13  46242  fourierdlem14  46243  fourierdlem34  46263  fourierdlem41  46270  fourierdlem48  46276  fourierdlem49  46277  fourierdlem54  46282  fourierdlem63  46291  fourierdlem64  46292  fourierdlem65  46293  fourierdlem69  46297  fourierdlem72  46300  fourierdlem74  46302  fourierdlem75  46303  fourierdlem79  46307  fourierdlem85  46313  fourierdlem88  46316  fourierdlem89  46317  fourierdlem90  46318  fourierdlem91  46319  fourierdlem92  46320  fourierdlem94  46322  fourierdlem97  46325  fourierdlem103  46331  fourierdlem104  46332  fourierdlem111  46339  fourierdlem113  46341  etransclem24  46380  etransclem26  46382  etransclem27  46383  etransclem28  46384  etransclem31  46387  etransclem32  46388  etransclem33  46389  etransclem34  46390  etransclem35  46391  etransclem37  46393  etransclem38  46394  rrxtopnfi  46409  rrndistlt  46412  qndenserrnbllem  46416  rrxsnicc  46422  ioorrnopnlem  46426  subsaliuncl  46480  hoicvr  46670  ovnprodcl  46676  ovnsupge0  46679  ovnlecvr  46680  ovncvrrp  46686  ovn0lem  46687  ovnsubaddlem1  46692  sge0hsphoire  46711  hoidmv1le  46716  hoidmvlelem1  46717  hoidmvlelem2  46718  hoidmvlelem3  46719  hoidmvlelem4  46720  hoidmvlelem5  46721  hoidmvle  46722  ovnhoilem2  46724  ovnlecvr2  46732  ovncvr2  46733  hoiqssbllem1  46744  hoiqssbllem2  46745  hoiqssbllem3  46746  hspmbllem2  46749  opnvonmbllem2  46755  ovolval2lem  46765  ovolval2  46766  ovolval3  46769  ovolval4lem2  46772  ovolval5lem3  46776  ovnovollem1  46778  ovnovollem2  46779  vonvolmbllem  46782  vonvolmbl2  46785  vonvol2  46786  snvonmbl  46808  vonsn  46813  iccpartxr  47543  nnsum4primeseven  47924  nnsum4primesevenALTV  47925  intop  48327  assintop  48333  isassintop  48334  ofaddmndmap  48467  rmsupp0  48492  domnmsuppn0  48493  rmsuppss  48494  scmsuppss  48495  gsumlsscl  48504  lincfsuppcl  48538  linccl  48539  lcosn0  48545  lincdifsn  48549  lincsum  48554  lincscm  48555  lincscmcl  48557  islinindfis  48574  lincext1  48579  lincext2  48580  lincext3  48581  lindslinindimp2lem1  48583  lindslinindimp2lem2  48584  lindslinindimp2lem4  48586  lindslinindsimp2lem5  48587  snlindsntor  48596  lincresunitlem2  48601  lincresunit3lem1  48604  lincresunit3lem2  48605  lincresunit3  48606  lincreslvec3  48607  isldepslvec2  48610  zlmodzxzldeplem2  48626  zlmodzxzldeplem3  48627  ldepsnlinclem1  48630  ldepsnlinclem2  48631  1arymaptf1  48767  1arymaptfo  48768  2arympt  48774  2arymaptf1  48778  2arymaptfo  48779  prelrrx2b  48839  eenglngeehlnmlem1  48862  eenglngeehlnmlem2  48863  aacllem  49926