Theorem elmapi 8789

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 8788	. . 3 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V))
2		elmapg 8779	. . 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 2114  Vcvv 3430  ⟶wf 6488  (class class class)co 7360   ↑_m cmap 8766

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7363  df-oprab 7364  df-mpo 7365  df-1st 7935  df-2nd 7936  df-map 8768

This theorem is referenced by:  mapfset  8790  elmapfn  8805  elmapfun  8806  elmapssres  8807  mapsspm  8817  mapfvd  8820  elmapresaun  8821  map0b  8824  mapss  8830  mapsncnv  8834  ralxpmap  8837  mapen  9072  mapxpen  9074  mapunen  9077  mapfienlem1  9311  mapfienlem2  9312  mapfienlem3  9313  mapfien  9314  wemaplem2  9455  wemappo  9457  wemapsolem  9458  wemapso  9459  wemapso2lem  9460  wemapwe  9609  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  10574  pwxpndom2  10579  ramval  16970  ramub  16975  ramcl  16991  prmgaplem7  17019  prmgaplem8  17020  imasdsval2  17471  funcf2  17826  funcpropd  17860  funcestrcsetclem8  18104  funcestrcsetclem9  18105  funcsetcestrclem8  18119  funcsetcestrclem9  18120  mndpsuppss  18724  mndvcl  18756  mndvass  18757  mndvlid  18758  mndvrid  18759  mhmvlin  18760  fsfnn0gsumfsffz  19949  gsummptnn0fzfv  19953  frlmfibas  21752  frlmbas3  21766  frlmipval  21769  frlmphllem  21770  frlmphl  21771  elfilspd  21793  islindf4  21828  psrbagf  21908  mplbas2  22030  ltbwe  22032  evlsvvvallem  22079  evlsvvval  22081  psr1baslem  22158  psr1basf  22175  fvcoe1  22181  coe1mul2lem1  22242  ply1coe  22273  mamures  22372  grpvlinv  22373  grpvrinv  22374  mamucl  22376  mamuass  22377  mamudi  22378  mamudir  22379  mamuvs1  22380  mamuvs2  22381  mamulid  22416  mamurid  22417  mattposcl  22428  mattpostpos  22429  tposmap  22432  mamutpos  22433  matgsumcl  22435  mavmulcl  22522  mavmulass  22524  mavmulsolcl  22526  marepvcl  22544  1marepvmarrepid  22550  mdetleib2  22563  mdetf  22570  mdetdiaglem  22573  mdetrlin  22577  mdetrsca  22578  mdetralt  22583  mdetunilem7  22593  mdetunilem9  22595  maducoeval2  22615  madutpos  22617  madugsum  22618  madurid  22619  cramerimplem1  22658  m2pmfzmap  22722  decpmatval  22740  pmatcollpw3lem  22758  pmatcollpw3fi1lem1  22761  pmatcollpw3fi1lem2  22762  pm2mp  22800  chfacfisf  22829  chfacfisfcpmat  22830  chfacfscmulgsum  22835  chfacfpmmulgsum  22839  chfacfpmmulgsum2  22840  cayhamlem1  22841  cpmadugsumlemF  22851  cpmadugsumfi  22852  cayhamlem2  22859  chcoeffeqlem  22860  cayleyhamilton1  22867  pnrmopn  23318  xkoptsub  23629  xkopt  23630  tmdgsum  24070  imasdsf1olem  24348  rrxnm  25368  rrxds  25370  rrxf  25378  rrxmvallem  25381  rrxbasefi  25387  rrxdsfi  25388  ehlbase  25392  ovolscalem2  25491  uniioombl  25566  tdeglem2  26036  plypf1  26187  ulmclm  26365  ulmcaulem  26372  ulmcau  26373  ulmss  26375  ulmbdd  26376  ulmcn  26377  ulmdvlem1  26378  ulmdvlem2  26379  ulmdvlem3  26380  mtest  26382  mtestbdd  26383  mbfulm  26384  iblulm  26385  itgulm  26386  itgulm2  26387  adjval2  31977  fmptco1f1o  32721  fcobijfs  32809  fcobijfs2  32810  resf1o  32818  fpwrelmap  32821  elrspunidl  33503  elrspunsn  33504  1arithidomlem2  33611  1arithidom  33612  fply1  33633  psrbasfsupp  33687  ply1degltdimlem  33782  fedgmullem1  33789  fedgmul  33791  extdg1id  33826  smatrcl  33956  mbfmf  34414  elmbfmvol2  34427  eulerpartlemelr  34517  eulerpartlemf  34530  eulerpartlemt  34531  eulerpartgbij  34532  eulerpartlemgu  34537  eulerpartlemgh  34538  eulerpartlemgf  34539  eulerpartlemgs2  34540  reprf  34772  reprsuc  34775  vtsprod  34799  circlemethhgt  34803  tgoldbachgtd  34822  satfv1lem  35560  satfvel  35610  satefvfmla0  35616  satefvfmla1  35623  prv1n  35629  mrsubff1  35712  mrsub0  35714  mrsubf  35715  mrsubccat  35716  mrsubcn  35717  msubrn  35727  msubff  35728  msubf  35730  msubff1  35754  mclsind  35768  uncf  37934  curunc  37937  unccur  37938  matunitlindflem1  37951  matunitlindflem2  37952  poimirlem4  37959  poimirlem5  37960  poimirlem6  37961  poimirlem7  37962  poimirlem8  37963  poimirlem10  37965  poimirlem11  37966  poimirlem12  37967  poimirlem16  37971  poimirlem17  37972  poimirlem18  37973  poimirlem19  37974  poimirlem20  37975  poimirlem21  37976  poimirlem22  37977  poimirlem25  37980  poimirlem26  37981  poimirlem27  37982  poimirlem29  37984  poimirlem30  37985  poimirlem31  37986  poimirlem32  37987  poimir  37988  broucube  37989  mblfinlem3  37994  mblfinlem4  37995  ismblfin  37996  rrnmet  38164  rrndstprj1  38165  rrndstprj2  38166  rrncmslem  38167  rrnequiv  38170  aks6d1c2lem4  42580  mapcod  42696  evlselv  43034  fsuppind  43037  mhphf  43044  mapco2g  43160  mapfzcons1  43163  mapfzcons2  43165  mzpcompact2lem  43197  eldiophb  43203  elmapresaunres2  43217  eq0rabdioph  43222  rexrabdioph  43240  eldioph4b  43257  diophren  43259  rmydioph  43460  rmxdioph  43462  expdiophlem2  43468  expdioph  43469  pw2f1o2val2  43486  wepwsolem  43488  pwfi2f1o  43542  ofoafo  43802  ofoaid1  43804  ofoaid2  43805  ofoaass  43806  ofoacom  43807  rfovcnvf1od  44449  rfovcnvfvd  44452  fsovrfovd  44454  fsovcnvlem  44458  ntrk0kbimka  44484  neik0pk1imk0  44492  ntrclsfveq1  44505  ntrclsfveq2  44506  ntrclsfveq  44507  ntrclsss  44508  ntrclsiso  44512  ntrclsk2  44513  ntrclskb  44514  ntrclsk3  44515  ntrclsk13  44516  ntrclsk4  44517  ntrneifv3  44527  ntrneineine0lem  44528  ntrneineine1lem  44529  ntrneifv4  44530  ntrneiel2  44531  ntrneicls00  44534  ntrneicls11  44535  ntrneiiso  44536  ntrneik2  44537  ntrneikb  44539  ntrneixb  44540  ntrneik3  44541  ntrneix3  44542  ntrneik13  44543  ntrneix13  44544  ntrneik4w  44545  ntrneik4  44546  clsneifv3  44555  clsneifv4  44556  neicvgfv  44566  k0004ss2  44597  k0004val0  44599  mnringbasefd  44663  mnugrud  44729  mapss2  45652  difmap  45654  inmap  45656  difmapsn  45659  ssmapsn  45663  mccllem  46045  dvnprodlem1  46392  dvnprodlem2  46393  fourierdlem11  46564  fourierdlem12  46565  fourierdlem13  46566  fourierdlem14  46567  fourierdlem34  46587  fourierdlem41  46594  fourierdlem48  46600  fourierdlem49  46601  fourierdlem54  46606  fourierdlem63  46615  fourierdlem64  46616  fourierdlem65  46617  fourierdlem69  46621  fourierdlem72  46624  fourierdlem74  46626  fourierdlem75  46627  fourierdlem79  46631  fourierdlem85  46637  fourierdlem88  46640  fourierdlem89  46641  fourierdlem90  46642  fourierdlem91  46643  fourierdlem92  46644  fourierdlem94  46646  fourierdlem97  46649  fourierdlem103  46655  fourierdlem104  46656  fourierdlem111  46663  fourierdlem113  46665  etransclem24  46704  etransclem26  46706  etransclem27  46707  etransclem28  46708  etransclem31  46711  etransclem32  46712  etransclem33  46713  etransclem34  46714  etransclem35  46715  etransclem37  46717  etransclem38  46718  rrxtopnfi  46733  rrndistlt  46736  qndenserrnbllem  46740  rrxsnicc  46746  ioorrnopnlem  46750  subsaliuncl  46804  hoicvr  46994  ovnprodcl  47000  ovnsupge0  47003  ovnlecvr  47004  ovncvrrp  47010  ovn0lem  47011  ovnsubaddlem1  47016  sge0hsphoire  47035  hoidmv1le  47040  hoidmvlelem1  47041  hoidmvlelem2  47042  hoidmvlelem3  47043  hoidmvlelem4  47044  hoidmvlelem5  47045  hoidmvle  47046  ovnhoilem2  47048  ovnlecvr2  47056  ovncvr2  47057  hoiqssbllem1  47068  hoiqssbllem2  47069  hoiqssbllem3  47070  hspmbllem2  47073  opnvonmbllem2  47079  ovolval2lem  47089  ovolval2  47090  ovolval3  47093  ovolval4lem2  47096  ovolval5lem3  47100  ovnovollem1  47102  ovnovollem2  47103  vonvolmbllem  47106  vonvolmbl2  47109  vonvol2  47110  snvonmbl  47132  vonsn  47137  iccpartxr  47891  nnsum4primeseven  48288  nnsum4primesevenALTV  48289  intop  48691  assintop  48697  isassintop  48698  ofaddmndmap  48831  rmsupp0  48856  domnmsuppn0  48857  rmsuppss  48858  scmsuppss  48859  gsumlsscl  48868  lincfsuppcl  48901  linccl  48902  lcosn0  48908  lincdifsn  48912  lincsum  48917  lincscm  48918  lincscmcl  48920  islinindfis  48937  lincext1  48942  lincext2  48943  lincext3  48944  lindslinindimp2lem1  48946  lindslinindimp2lem2  48947  lindslinindimp2lem4  48949  lindslinindsimp2lem5  48950  snlindsntor  48959  lincresunitlem2  48964  lincresunit3lem1  48967  lincresunit3lem2  48968  lincresunit3  48969  lincreslvec3  48970  isldepslvec2  48973  zlmodzxzldeplem2  48989  zlmodzxzldeplem3  48990  ldepsnlinclem1  48993  ldepsnlinclem2  48994  1arymaptf1  49130  1arymaptfo  49131  2arympt  49137  2arymaptf1  49141  2arymaptfo  49142  prelrrx2b  49202  eenglngeehlnmlem1  49225  eenglngeehlnmlem2  49226  aacllem  50288