Theorem elmapi 8840

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   ∈ wcel 2107  Vcvv 3475  ⟶wf 6537  (class class class)co 7406   ↑_m cmap 8817

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-fv 6549  df-ov 7409  df-oprab 7410  df-mpo 7411  df-1st 7972  df-2nd 7973  df-map 8819

This theorem is referenced by:  mapfset  8841  elmapfn  8856  elmapfun  8857  elmapssres  8858  mapsspm  8867  mapfvd  8870  elmapresaun  8871  map0b  8874  mapss  8880  mapsncnv  8884  ralxpmap  8887  mapen  9138  mapxpen  9140  mapunen  9143  mapfienlem1  9397  mapfienlem2  9398  mapfienlem3  9399  mapfien  9400  wemaplem2  9539  wemappo  9541  wemapsolem  9542  wemapso  9543  wemapso2lem  9544  wemapwe  9689  iunmapdisj  10015  fseqenlem1  10016  fseqenlem2  10017  numacn  10041  finacn  10042  acndom  10043  acndom2  10046  infpwfien  10054  infmap2  10210  fin23lem40  10343  isf32lem12  10356  isf34lem6  10372  acncc  10432  pwfseqlem3  10652  pwxpndom2  10657  ramval  16938  ramub  16943  ramcl  16959  prmgaplem7  16987  prmgaplem8  16988  imasdsval2  17459  funcf2  17815  funcpropd  17848  funcestrcsetclem8  18096  funcestrcsetclem9  18097  funcsetcestrclem8  18111  funcsetcestrclem9  18112  fsfnn0gsumfsffz  19846  gsummptnn0fzfv  19850  frlmfibas  21309  frlmbas3  21323  frlmipval  21326  frlmphllem  21327  frlmphl  21328  elfilspd  21350  islindf4  21385  psrbagf  21463  mplbas2  21589  ltbwe  21591  psr1baslem  21701  psr1basf  21717  fvcoe1  21723  coe1mul2lem1  21781  ply1coe  21812  mamures  21884  mndvcl  21885  mndvass  21886  mndvlid  21887  mndvrid  21888  grpvlinv  21889  grpvrinv  21890  mhmvlin  21891  mamucl  21893  mamuass  21894  mamudi  21895  mamudir  21896  mamuvs1  21897  mamuvs2  21898  mamulid  21935  mamurid  21936  mattposcl  21947  mattpostpos  21948  tposmap  21951  mamutpos  21952  matgsumcl  21954  mavmulcl  22041  mavmulass  22043  mavmulsolcl  22045  marepvcl  22063  1marepvmarrepid  22069  mdetleib2  22082  mdetf  22089  mdetdiaglem  22092  mdetrlin  22096  mdetrsca  22097  mdetralt  22102  mdetunilem7  22112  mdetunilem9  22114  maducoeval2  22134  madutpos  22136  madugsum  22137  madurid  22138  cramerimplem1  22177  m2pmfzmap  22241  decpmatval  22259  pmatcollpw3lem  22277  pmatcollpw3fi1lem1  22280  pmatcollpw3fi1lem2  22281  pm2mp  22319  chfacfisf  22348  chfacfisfcpmat  22349  chfacfscmulgsum  22354  chfacfpmmulgsum  22358  chfacfpmmulgsum2  22359  cayhamlem1  22360  cpmadugsumlemF  22370  cpmadugsumfi  22371  cayhamlem2  22378  chcoeffeqlem  22379  cayleyhamilton1  22386  pnrmopn  22839  xkoptsub  23150  xkopt  23151  tmdgsum  23591  imasdsf1olem  23871  rrxnm  24900  rrxds  24902  rrxf  24910  rrxmvallem  24913  rrxbasefi  24919  rrxdsfi  24920  ehlbase  24924  ovolscalem2  25023  uniioombl  25098  tdeglem2  25571  plypf1  25718  ulmclm  25891  ulmcaulem  25898  ulmcau  25899  ulmss  25901  ulmbdd  25902  ulmcn  25903  ulmdvlem1  25904  ulmdvlem2  25905  ulmdvlem3  25906  mtest  25908  mtestbdd  25909  mbfulm  25910  iblulm  25911  itgulm  25912  itgulm2  25913  adjval2  31132  fmptco1f1o  31845  fcobijfs  31936  resf1o  31943  fpwrelmap  31946  elrspunidl  32535  elrspunsn  32536  fply1  32626  ply1degltdimlem  32696  fedgmullem1  32703  fedgmul  32705  extdg1id  32731  smatrcl  32765  mbfmf  33241  elmbfmvol2  33255  eulerpartlemelr  33345  eulerpartlemf  33358  eulerpartlemt  33359  eulerpartgbij  33360  eulerpartlemgu  33365  eulerpartlemgh  33366  eulerpartlemgf  33367  eulerpartlemgs2  33368  reprf  33613  reprsuc  33616  vtsprod  33640  circlemethhgt  33644  tgoldbachgtd  33663  satfv1lem  34342  satfvel  34392  satefvfmla0  34398  satefvfmla1  34405  prv1n  34411  mrsubff1  34494  mrsub0  34496  mrsubf  34497  mrsubccat  34498  mrsubcn  34499  msubrn  34509  msubff  34510  msubf  34512  msubff1  34536  mclsind  34550  uncf  36456  curunc  36459  unccur  36460  matunitlindflem1  36473  matunitlindflem2  36474  poimirlem4  36481  poimirlem5  36482  poimirlem6  36483  poimirlem7  36484  poimirlem8  36485  poimirlem10  36487  poimirlem11  36488  poimirlem12  36489  poimirlem16  36493  poimirlem17  36494  poimirlem18  36495  poimirlem19  36496  poimirlem20  36497  poimirlem21  36498  poimirlem22  36499  poimirlem25  36502  poimirlem26  36503  poimirlem27  36504  poimirlem29  36506  poimirlem30  36507  poimirlem31  36508  poimirlem32  36509  poimir  36510  broucube  36511  mblfinlem3  36516  mblfinlem4  36517  ismblfin  36518  rrnmet  36686  rrndstprj1  36687  rrndstprj2  36688  rrncmslem  36689  rrnequiv  36692  mapcod  41065  evlsvvvallem  41131  evlsvvval  41133  evlselv  41157  fsuppind  41160  mhphf  41167  mapco2g  41438  mapfzcons1  41441  mapfzcons2  41443  mzpcompact2lem  41475  eldiophb  41481  elmapresaunres2  41495  eq0rabdioph  41500  rexrabdioph  41518  eldioph4b  41535  diophren  41537  rmydioph  41739  rmxdioph  41741  expdiophlem2  41747  expdioph  41748  pw2f1o2val2  41765  wepwsolem  41770  pwfi2f1o  41824  ofoafo  42092  ofoaid1  42094  ofoaid2  42095  ofoaass  42096  ofoacom  42097  rfovcnvf1od  42741  rfovcnvfvd  42744  fsovrfovd  42746  fsovcnvlem  42750  ntrk0kbimka  42776  neik0pk1imk0  42784  ntrclsfveq1  42797  ntrclsfveq2  42798  ntrclsfveq  42799  ntrclsss  42800  ntrclsiso  42804  ntrclsk2  42805  ntrclskb  42806  ntrclsk3  42807  ntrclsk13  42808  ntrclsk4  42809  ntrneifv3  42819  ntrneineine0lem  42820  ntrneineine1lem  42821  ntrneifv4  42822  ntrneiel2  42823  ntrneicls00  42826  ntrneicls11  42827  ntrneiiso  42828  ntrneik2  42829  ntrneikb  42831  ntrneixb  42832  ntrneik3  42833  ntrneix3  42834  ntrneik13  42835  ntrneix13  42836  ntrneik4w  42837  ntrneik4  42838  clsneifv3  42847  clsneifv4  42848  neicvgfv  42858  k0004ss2  42889  k0004val0  42891  mnringbasefd  42960  mnugrud  43029  mapss2  43890  difmap  43892  inmap  43894  difmapsn  43897  ssmapsn  43901  mccllem  44300  dvnprodlem1  44649  dvnprodlem2  44650  fourierdlem11  44821  fourierdlem12  44822  fourierdlem13  44823  fourierdlem14  44824  fourierdlem34  44844  fourierdlem41  44851  fourierdlem48  44857  fourierdlem49  44858  fourierdlem54  44863  fourierdlem63  44872  fourierdlem64  44873  fourierdlem65  44874  fourierdlem69  44878  fourierdlem72  44881  fourierdlem74  44883  fourierdlem75  44884  fourierdlem79  44888  fourierdlem85  44894  fourierdlem88  44897  fourierdlem89  44898  fourierdlem90  44899  fourierdlem91  44900  fourierdlem92  44901  fourierdlem94  44903  fourierdlem97  44906  fourierdlem103  44912  fourierdlem104  44913  fourierdlem111  44920  fourierdlem113  44922  etransclem24  44961  etransclem26  44963  etransclem27  44964  etransclem28  44965  etransclem31  44968  etransclem32  44969  etransclem33  44970  etransclem34  44971  etransclem35  44972  etransclem37  44974  etransclem38  44975  rrxtopnfi  44990  rrndistlt  44993  qndenserrnbllem  44997  rrxsnicc  45003  ioorrnopnlem  45007  subsaliuncl  45061  hoicvr  45251  ovnprodcl  45257  ovnsupge0  45260  ovnlecvr  45261  ovncvrrp  45267  ovn0lem  45268  ovnsubaddlem1  45273  sge0hsphoire  45292  hoidmv1le  45297  hoidmvlelem1  45298  hoidmvlelem2  45299  hoidmvlelem3  45300  hoidmvlelem4  45301  hoidmvlelem5  45302  hoidmvle  45303  ovnhoilem2  45305  ovnlecvr2  45313  ovncvr2  45314  hoiqssbllem1  45325  hoiqssbllem2  45326  hoiqssbllem3  45327  hspmbllem2  45330  opnvonmbllem2  45336  ovolval2lem  45346  ovolval2  45347  ovolval3  45350  ovolval4lem2  45353  ovolval5lem3  45357  ovnovollem1  45359  ovnovollem2  45360  vonvolmbllem  45363  vonvolmbl2  45366  vonvol2  45367  snvonmbl  45389  vonsn  45394  iccpartxr  46074  nnsum4primeseven  46455  nnsum4primesevenALTV  46456  intop  46600  assintop  46606  isassintop  46607  ofaddmndmap  46973  rmsupp0  46998  domnmsuppn0  46999  rmsuppss  47000  mndpsuppss  47001  scmsuppss  47002  gsumlsscl  47013  lincfsuppcl  47048  linccl  47049  lcosn0  47055  lincdifsn  47059  lincsum  47064  lincscm  47065  lincscmcl  47067  islinindfis  47084  lincext1  47089  lincext2  47090  lincext3  47091  lindslinindimp2lem1  47093  lindslinindimp2lem2  47094  lindslinindimp2lem4  47096  lindslinindsimp2lem5  47097  snlindsntor  47106  lincresunitlem2  47111  lincresunit3lem1  47114  lincresunit3lem2  47115  lincresunit3  47116  lincreslvec3  47117  isldepslvec2  47120  zlmodzxzldeplem2  47136  zlmodzxzldeplem3  47137  ldepsnlinclem1  47140  ldepsnlinclem2  47141  1arymaptf1  47282  1arymaptfo  47283  2arympt  47289  2arymaptf1  47293  2arymaptfo  47294  prelrrx2b  47354  eenglngeehlnmlem1  47377  eenglngeehlnmlem2  47378  aacllem  47802