Theorem elmapi 8826

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∈ wcel 2141  Vcvv 3453  ⟶wf 6513  (class class class)co 7392   ↑_m cmap 8803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pow 5321  ax-pr 5389  ax-un 7714

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-iun 4950  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-fv 6525  df-ov 7395  df-oprab 7396  df-mpo 7397  df-1st 7966  df-2nd 7967  df-map 8805

This theorem is referenced by:  mapfset  8827  elmapfn  8842  elmapfun  8843  elmapssres  8844  mapsspm  8854  mapfvd  8857  elmapresaun  8858  map0b  8861  mapss  8867  mapsncnv  8871  ralxpmap  8874  mapen  9109  mapxpen  9111  mapunen  9114  mapfienlem1  9348  mapfienlem2  9349  mapfienlem3  9350  mapfien  9351  wemaplem2  9492  wemappo  9494  wemapsolem  9495  wemapso  9496  wemapso2lem  9497  wemapwe  9649  iunmapdisj  9976  fseqenlem1  9977  fseqenlem2  9978  numacn  10002  finacn  10003  acndom  10004  acndom2  10007  infpwfien  10015  infmap2  10170  fin23lem40  10305  isf32lem12  10318  isf34lem6  10334  acncc  10394  pwfseqlem3  10615  pwxpndom2  10620  ramval  17027  ramub  17032  ramcl  17048  prmgaplem7  17076  prmgaplem8  17077  imasdsval2  17529  funcf2  17884  funcpropd  17918  funcestrcsetclem8  18162  funcestrcsetclem9  18163  funcsetcestrclem8  18177  funcsetcestrclem9  18178  mndpsuppss  18782  mndvcl  18814  mndvass  18815  mndvlid  18816  mndvrid  18817  mhmvlin  18818  fsfnn0gsumfsffz  20006  gsummptnn0fzfv  20010  frlmfibas  21794  frlmbas3  21808  frlmipval  21811  frlmphllem  21812  frlmphl  21813  elfilspd  21835  islindf4  21870  psrbagf  21950  mplbas2  22075  ltbwe  22077  evlsvvvallem  22124  evlsvvval  22126  psr1baslem  22227  psr1basf  22243  fvcoe1  22249  coe1mul2lem1  22310  ply1coe  22341  mamures  22437  grpvlinv  22438  grpvrinv  22439  mamucl  22441  mamuass  22442  mamudi  22443  mamudir  22444  mamuvs1  22445  mamuvs2  22446  mamulid  22481  mamurid  22482  mattposcl  22493  mattpostpos  22494  tposmap  22497  mamutpos  22498  matgsumcl  22500  mavmulcl  22587  mavmulass  22589  mavmulsolcl  22591  marepvcl  22609  1marepvmarrepid  22615  mdetleib2  22628  mdetf  22635  mdetdiaglem  22638  mdetrlin  22642  mdetrsca  22643  mdetralt  22648  mdetunilem7  22658  mdetunilem9  22660  maducoeval2  22680  madutpos  22682  madugsum  22683  madurid  22684  cramerimplem1  22723  m2pmfzmap  22787  decpmatval  22805  pmatcollpw3lem  22823  pmatcollpw3fi1lem1  22826  pmatcollpw3fi1lem2  22827  pm2mp  22865  chfacfisf  22894  chfacfisfcpmat  22895  chfacfscmulgsum  22900  chfacfpmmulgsum  22904  chfacfpmmulgsum2  22905  cayhamlem1  22906  cpmadugsumlemF  22916  cpmadugsumfi  22917  cayhamlem2  22924  chcoeffeqlem  22925  cayleyhamilton1  22932  pnrmopn  23383  xkoptsub  23694  xkopt  23695  tmdgsum  24135  imasdsf1olem  24413  rrxnm  25433  rrxds  25435  rrxf  25443  rrxmvallem  25446  rrxbasefi  25452  rrxdsfi  25453  ehlbase  25457  ovolscalem2  25556  uniioombl  25631  tdeglem2  26101  plypf1  26252  ulmclm  26427  ulmcaulem  26434  ulmcau  26435  ulmss  26437  ulmbdd  26438  ulmcn  26439  ulmdvlem1  26440  ulmdvlem2  26441  ulmdvlem3  26442  mtest  26444  mtestbdd  26445  mbfulm  26446  iblulm  26447  itgulm  26448  itgulm2  26449  adjval2  32040  fmptco1f1o  32785  fcobijfs  32873  fcobijfs2  32874  resf1o  32882  fpwrelmap  32885  elrspunidl  33575  elrspunsn  33576  1arithidomlem2  33693  1arithidom  33694  fply1  33715  psrbasfsupp  33769  selvply1rhmlemb  33777  ply1degltdimlem  33880  fedgmullem1  33887  fedgmul  33889  extdg1id  33924  smatrcl  34054  mbfmf  34512  elmbfmvol2  34525  eulerpartlemelr  34615  eulerpartlemf  34628  eulerpartlemt  34629  eulerpartgbij  34630  eulerpartlemgu  34635  eulerpartlemgh  34636  eulerpartlemgf  34637  eulerpartlemgs2  34638  reprf  34870  reprsuc  34873  vtsprod  34897  circlemethhgt  34901  tgoldbachgtd  34920  satfv1lem  35676  satfvel  35726  satefvfmla0  35732  satefvfmla1  35739  prv1n  35745  mrsubff1  35828  mrsub0  35830  mrsubf  35831  mrsubccat  35832  mrsubcn  35833  msubrn  35843  msubff  35844  msubf  35846  msubff1  35870  mclsind  35884  uncf  38062  curunc  38065  unccur  38066  matunitlindflem1  38079  matunitlindflem2  38080  poimirlem4  38087  poimirlem5  38088  poimirlem6  38089  poimirlem7  38090  poimirlem8  38091  poimirlem10  38093  poimirlem11  38094  poimirlem12  38095  poimirlem16  38099  poimirlem17  38100  poimirlem18  38101  poimirlem19  38102  poimirlem20  38103  poimirlem21  38104  poimirlem22  38105  poimirlem25  38108  poimirlem26  38109  poimirlem27  38110  poimirlem29  38112  poimirlem30  38113  poimirlem31  38114  poimirlem32  38115  poimir  38116  broucube  38117  mblfinlem3  38122  mblfinlem4  38123  ismblfin  38124  rrnmet  38292  rrndstprj1  38293  rrndstprj2  38294  rrncmslem  38295  rrnequiv  38298  aks6d1c2lem4  42708  mapcod  42823  evlselv  43135  fsuppind  43136  mhphf  43143  mapco2g  43259  mapfzcons1  43262  mapfzcons2  43264  mzpcompact2lem  43296  eldiophb  43302  elmapresaunres2  43316  eq0rabdioph  43321  rexrabdioph  43335  eldioph4b  43352  diophren  43354  rmydioph  43555  rmxdioph  43557  expdiophlem2  43563  expdioph  43564  pw2f1o2val2  43581  wepwsolem  43583  pwfi2f1o  43637  ofoafo  43897  ofoaid1  43899  ofoaid2  43900  ofoaass  43901  ofoacom  43902  rfovcnvf1od  44544  rfovcnvfvd  44547  fsovrfovd  44549  fsovcnvlem  44553  ntrk0kbimka  44579  neik0pk1imk0  44587  ntrclsfveq1  44600  ntrclsfveq2  44601  ntrclsfveq  44602  ntrclsss  44603  ntrclsiso  44607  ntrclsk2  44608  ntrclskb  44609  ntrclsk3  44610  ntrclsk13  44611  ntrclsk4  44612  ntrneifv3  44622  ntrneineine0lem  44623  ntrneineine1lem  44624  ntrneifv4  44625  ntrneiel2  44626  ntrneicls00  44629  ntrneicls11  44630  ntrneiiso  44631  ntrneik2  44632  ntrneikb  44634  ntrneixb  44635  ntrneik3  44636  ntrneix3  44637  ntrneik13  44638  ntrneix13  44639  ntrneik4w  44640  ntrneik4  44641  clsneifv3  44650  clsneifv4  44651  neicvgfv  44661  k0004ss2  44692  k0004val0  44694  mnringbasefd  44758  mnugrud  44824  mapss2  45746  difmap  45747  inmap  45749  difmapsn  45752  ssmapsn  45756  mccllem  46137  dvnprodlem1  46484  dvnprodlem2  46485  fourierdlem11  46656  fourierdlem12  46657  fourierdlem13  46658  fourierdlem14  46659  fourierdlem34  46679  fourierdlem41  46686  fourierdlem48  46692  fourierdlem49  46693  fourierdlem54  46698  fourierdlem63  46707  fourierdlem64  46708  fourierdlem65  46709  fourierdlem69  46713  fourierdlem72  46716  fourierdlem74  46718  fourierdlem75  46719  fourierdlem79  46723  fourierdlem85  46729  fourierdlem88  46732  fourierdlem89  46733  fourierdlem90  46734  fourierdlem91  46735  fourierdlem92  46736  fourierdlem94  46738  fourierdlem97  46741  fourierdlem103  46747  fourierdlem104  46748  fourierdlem111  46755  fourierdlem113  46757  etransclem24  46796  etransclem26  46798  etransclem27  46799  etransclem28  46800  etransclem31  46803  etransclem32  46804  etransclem33  46805  etransclem34  46806  etransclem35  46807  etransclem37  46809  etransclem38  46810  rrxtopnfi  46825  rrndistlt  46828  qndenserrnbllem  46832  rrxsnicc  46838  ioorrnopnlem  46842  subsaliuncl  46896  hoicvr  47086  ovnprodcl  47092  ovnsupge0  47095  ovnlecvr  47096  ovncvrrp  47102  ovn0lem  47103  ovnsubaddlem1  47108  sge0hsphoire  47127  hoidmv1le  47132  hoidmvlelem1  47133  hoidmvlelem2  47134  hoidmvlelem3  47135  hoidmvlelem4  47136  hoidmvlelem5  47137  hoidmvle  47138  ovnhoilem2  47140  ovnlecvr2  47148  ovncvr2  47149  hoiqssbllem1  47160  hoiqssbllem2  47161  hoiqssbllem3  47162  hspmbllem2  47165  opnvonmbllem2  47171  ovolval2lem  47181  ovolval2  47182  ovolval3  47185  ovolval4lem2  47188  ovolval5lem3  47192  ovnovollem1  47194  ovnovollem2  47195  vonvolmbllem  47198  vonvolmbl2  47201  vonvol2  47202  snvonmbl  47224  vonsn  47229  iccpartxr  47989  nnsum4primeseven  48386  nnsum4primesevenALTV  48387  intop  48789  assintop  48795  isassintop  48796  ofaddmndmap  48929  rmsupp0  48954  domnmsuppn0  48955  rmsuppss  48956  scmsuppss  48957  gsumlsscl  48966  lincfsuppcl  48999  linccl  49000  lcosn0  49006  lincdifsn  49010  lincsum  49015  lincscm  49016  lincscmcl  49018  islinindfis  49035  lincext1  49040  lincext2  49041  lincext3  49042  lindslinindimp2lem1  49044  lindslinindimp2lem2  49045  lindslinindimp2lem4  49047  lindslinindsimp2lem5  49048  snlindsntor  49057  lincresunitlem2  49062  lincresunit3lem1  49065  lincresunit3lem2  49066  lincresunit3  49067  lincreslvec3  49068  isldepslvec2  49071  zlmodzxzldeplem2  49087  zlmodzxzldeplem3  49088  ldepsnlinclem1  49091  ldepsnlinclem2  49092  1arymaptf1  49228  1arymaptfo  49229  2arympt  49235  2arymaptf1  49239  2arymaptfo  49240  prelrrx2b  49300  eenglngeehlnmlem1  49323  eenglngeehlnmlem2  49324  aacllem  50386