Theorem elmapi 8783

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 8782	. . 3 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V))
2		elmapg 8773	. . 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 2109  Vcvv 3438  ⟶wf 6482  (class class class)co 7353   ↑_m cmap 8760

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-fv 6494  df-ov 7356  df-oprab 7357  df-mpo 7358  df-1st 7931  df-2nd 7932  df-map 8762

This theorem is referenced by:  mapfset  8784  elmapfn  8799  elmapfun  8800  elmapssres  8801  mapsspm  8810  mapfvd  8813  elmapresaun  8814  map0b  8817  mapss  8823  mapsncnv  8827  ralxpmap  8830  mapen  9065  mapxpen  9067  mapunen  9070  mapfienlem1  9314  mapfienlem2  9315  mapfienlem3  9316  mapfien  9317  wemaplem2  9458  wemappo  9460  wemapsolem  9461  wemapso  9462  wemapso2lem  9463  wemapwe  9612  iunmapdisj  9936  fseqenlem1  9937  fseqenlem2  9938  numacn  9962  finacn  9963  acndom  9964  acndom2  9967  infpwfien  9975  infmap2  10130  fin23lem40  10264  isf32lem12  10277  isf34lem6  10293  acncc  10353  pwfseqlem3  10573  pwxpndom2  10578  ramval  16938  ramub  16943  ramcl  16959  prmgaplem7  16987  prmgaplem8  16988  imasdsval2  17438  funcf2  17793  funcpropd  17827  funcestrcsetclem8  18071  funcestrcsetclem9  18072  funcsetcestrclem8  18086  funcsetcestrclem9  18087  mndpsuppss  18657  mndvcl  18689  mndvass  18690  mndvlid  18691  mndvrid  18692  mhmvlin  18693  fsfnn0gsumfsffz  19880  gsummptnn0fzfv  19884  frlmfibas  21687  frlmbas3  21701  frlmipval  21704  frlmphllem  21705  frlmphl  21706  elfilspd  21728  islindf4  21763  psrbagf  21843  mplbas2  21965  ltbwe  21967  psr1baslem  22085  psr1basf  22102  fvcoe1  22108  coe1mul2lem1  22169  ply1coe  22201  mamures  22300  grpvlinv  22301  grpvrinv  22302  mamucl  22304  mamuass  22305  mamudi  22306  mamudir  22307  mamuvs1  22308  mamuvs2  22309  mamulid  22344  mamurid  22345  mattposcl  22356  mattpostpos  22357  tposmap  22360  mamutpos  22361  matgsumcl  22363  mavmulcl  22450  mavmulass  22452  mavmulsolcl  22454  marepvcl  22472  1marepvmarrepid  22478  mdetleib2  22491  mdetf  22498  mdetdiaglem  22501  mdetrlin  22505  mdetrsca  22506  mdetralt  22511  mdetunilem7  22521  mdetunilem9  22523  maducoeval2  22543  madutpos  22545  madugsum  22546  madurid  22547  cramerimplem1  22586  m2pmfzmap  22650  decpmatval  22668  pmatcollpw3lem  22686  pmatcollpw3fi1lem1  22689  pmatcollpw3fi1lem2  22690  pm2mp  22728  chfacfisf  22757  chfacfisfcpmat  22758  chfacfscmulgsum  22763  chfacfpmmulgsum  22767  chfacfpmmulgsum2  22768  cayhamlem1  22769  cpmadugsumlemF  22779  cpmadugsumfi  22780  cayhamlem2  22787  chcoeffeqlem  22788  cayleyhamilton1  22795  pnrmopn  23246  xkoptsub  23557  xkopt  23558  tmdgsum  23998  imasdsf1olem  24277  rrxnm  25307  rrxds  25309  rrxf  25317  rrxmvallem  25320  rrxbasefi  25326  rrxdsfi  25327  ehlbase  25331  ovolscalem2  25431  uniioombl  25506  tdeglem2  25982  plypf1  26133  ulmclm  26312  ulmcaulem  26319  ulmcau  26320  ulmss  26322  ulmbdd  26323  ulmcn  26324  ulmdvlem1  26325  ulmdvlem2  26326  ulmdvlem3  26327  mtest  26329  mtestbdd  26330  mbfulm  26331  iblulm  26332  itgulm  26333  itgulm2  26334  adjval2  31853  fmptco1f1o  32590  fcobijfs  32679  resf1o  32686  fpwrelmap  32689  elrspunidl  33375  elrspunsn  33376  1arithidomlem2  33483  1arithidom  33484  fply1  33503  ply1degltdimlem  33594  fedgmullem1  33601  fedgmul  33603  extdg1id  33637  smatrcl  33762  mbfmf  34220  elmbfmvol2  34234  eulerpartlemelr  34324  eulerpartlemf  34337  eulerpartlemt  34338  eulerpartgbij  34339  eulerpartlemgu  34344  eulerpartlemgh  34345  eulerpartlemgf  34346  eulerpartlemgs2  34347  reprf  34579  reprsuc  34582  vtsprod  34606  circlemethhgt  34610  tgoldbachgtd  34629  satfv1lem  35334  satfvel  35384  satefvfmla0  35390  satefvfmla1  35397  prv1n  35403  mrsubff1  35486  mrsub0  35488  mrsubf  35489  mrsubccat  35490  mrsubcn  35491  msubrn  35501  msubff  35502  msubf  35504  msubff1  35528  mclsind  35542  uncf  37578  curunc  37581  unccur  37582  matunitlindflem1  37595  matunitlindflem2  37596  poimirlem4  37603  poimirlem5  37604  poimirlem6  37605  poimirlem7  37606  poimirlem8  37607  poimirlem10  37609  poimirlem11  37610  poimirlem12  37611  poimirlem16  37615  poimirlem17  37616  poimirlem18  37617  poimirlem19  37618  poimirlem20  37619  poimirlem21  37620  poimirlem22  37621  poimirlem25  37624  poimirlem26  37625  poimirlem27  37626  poimirlem29  37628  poimirlem30  37629  poimirlem31  37630  poimirlem32  37631  poimir  37632  broucube  37633  mblfinlem3  37638  mblfinlem4  37639  ismblfin  37640  rrnmet  37808  rrndstprj1  37809  rrndstprj2  37810  rrncmslem  37811  rrnequiv  37814  aks6d1c2lem4  42100  mapcod  42216  evlsvvvallem  42534  evlsvvval  42536  evlselv  42560  fsuppind  42563  mhphf  42570  mapco2g  42687  mapfzcons1  42690  mapfzcons2  42692  mzpcompact2lem  42724  eldiophb  42730  elmapresaunres2  42744  eq0rabdioph  42749  rexrabdioph  42767  eldioph4b  42784  diophren  42786  rmydioph  42987  rmxdioph  42989  expdiophlem2  42995  expdioph  42996  pw2f1o2val2  43013  wepwsolem  43015  pwfi2f1o  43069  ofoafo  43329  ofoaid1  43331  ofoaid2  43332  ofoaass  43333  ofoacom  43334  rfovcnvf1od  43977  rfovcnvfvd  43980  fsovrfovd  43982  fsovcnvlem  43986  ntrk0kbimka  44012  neik0pk1imk0  44020  ntrclsfveq1  44033  ntrclsfveq2  44034  ntrclsfveq  44035  ntrclsss  44036  ntrclsiso  44040  ntrclsk2  44041  ntrclskb  44042  ntrclsk3  44043  ntrclsk13  44044  ntrclsk4  44045  ntrneifv3  44055  ntrneineine0lem  44056  ntrneineine1lem  44057  ntrneifv4  44058  ntrneiel2  44059  ntrneicls00  44062  ntrneicls11  44063  ntrneiiso  44064  ntrneik2  44065  ntrneikb  44067  ntrneixb  44068  ntrneik3  44069  ntrneix3  44070  ntrneik13  44071  ntrneix13  44072  ntrneik4w  44073  ntrneik4  44074  clsneifv3  44083  clsneifv4  44084  neicvgfv  44094  k0004ss2  44125  k0004val0  44127  mnringbasefd  44191  mnugrud  44257  mapss2  45183  difmap  45185  inmap  45187  difmapsn  45190  ssmapsn  45194  mccllem  45579  dvnprodlem1  45928  dvnprodlem2  45929  fourierdlem11  46100  fourierdlem12  46101  fourierdlem13  46102  fourierdlem14  46103  fourierdlem34  46123  fourierdlem41  46130  fourierdlem48  46136  fourierdlem49  46137  fourierdlem54  46142  fourierdlem63  46151  fourierdlem64  46152  fourierdlem65  46153  fourierdlem69  46157  fourierdlem72  46160  fourierdlem74  46162  fourierdlem75  46163  fourierdlem79  46167  fourierdlem85  46173  fourierdlem88  46176  fourierdlem89  46177  fourierdlem90  46178  fourierdlem91  46179  fourierdlem92  46180  fourierdlem94  46182  fourierdlem97  46185  fourierdlem103  46191  fourierdlem104  46192  fourierdlem111  46199  fourierdlem113  46201  etransclem24  46240  etransclem26  46242  etransclem27  46243  etransclem28  46244  etransclem31  46247  etransclem32  46248  etransclem33  46249  etransclem34  46250  etransclem35  46251  etransclem37  46253  etransclem38  46254  rrxtopnfi  46269  rrndistlt  46272  qndenserrnbllem  46276  rrxsnicc  46282  ioorrnopnlem  46286  subsaliuncl  46340  hoicvr  46530  ovnprodcl  46536  ovnsupge0  46539  ovnlecvr  46540  ovncvrrp  46546  ovn0lem  46547  ovnsubaddlem1  46552  sge0hsphoire  46571  hoidmv1le  46576  hoidmvlelem1  46577  hoidmvlelem2  46578  hoidmvlelem3  46579  hoidmvlelem4  46580  hoidmvlelem5  46581  hoidmvle  46582  ovnhoilem2  46584  ovnlecvr2  46592  ovncvr2  46593  hoiqssbllem1  46604  hoiqssbllem2  46605  hoiqssbllem3  46606  hspmbllem2  46609  opnvonmbllem2  46615  ovolval2lem  46625  ovolval2  46626  ovolval3  46629  ovolval4lem2  46632  ovolval5lem3  46636  ovnovollem1  46638  ovnovollem2  46639  vonvolmbllem  46642  vonvolmbl2  46645  vonvol2  46646  snvonmbl  46668  vonsn  46673  iccpartxr  47404  nnsum4primeseven  47785  nnsum4primesevenALTV  47786  intop  48188  assintop  48194  isassintop  48195  ofaddmndmap  48328  rmsupp0  48353  domnmsuppn0  48354  rmsuppss  48355  scmsuppss  48356  gsumlsscl  48365  lincfsuppcl  48399  linccl  48400  lcosn0  48406  lincdifsn  48410  lincsum  48415  lincscm  48416  lincscmcl  48418  islinindfis  48435  lincext1  48440  lincext2  48441  lincext3  48442  lindslinindimp2lem1  48444  lindslinindimp2lem2  48445  lindslinindimp2lem4  48447  lindslinindsimp2lem5  48448  snlindsntor  48457  lincresunitlem2  48462  lincresunit3lem1  48465  lincresunit3lem2  48466  lincresunit3  48467  lincreslvec3  48468  isldepslvec2  48471  zlmodzxzldeplem2  48487  zlmodzxzldeplem3  48488  ldepsnlinclem1  48491  ldepsnlinclem2  48492  1arymaptf1  48628  1arymaptfo  48629  2arympt  48635  2arymaptf1  48639  2arymaptfo  48640  prelrrx2b  48700  eenglngeehlnmlem1  48723  eenglngeehlnmlem2  48724  aacllem  49787