Theorem elmapi 8411

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∈ wcel 2111  Vcvv 3441  ⟶wf 6320  (class class class)co 7135   ↑_m cmap 8389

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-fv 6332  df-ov 7138  df-oprab 7139  df-mpo 7140  df-1st 7671  df-2nd 7672  df-map 8391

This theorem is referenced by:  elmapfn  8412  elmapfun  8413  elmapssres  8414  mapsspm  8423  mapfvd  8426  elmapresaun  8427  map0b  8430  mapss  8436  mapsncnv  8440  ralxpmap  8443  mapen  8665  mapxpen  8667  mapunen  8670  mapfienlem1  8852  mapfienlem2  8853  mapfienlem3  8854  mapfien  8855  wemaplem2  8995  wemappo  8997  wemapsolem  8998  wemapso  8999  wemapso2lem  9000  wemapwe  9144  iunmapdisj  9434  fseqenlem1  9435  fseqenlem2  9436  numacn  9460  finacn  9461  acndom  9462  acndom2  9465  infpwfien  9473  infmap2  9629  fin23lem40  9762  isf32lem12  9775  isf34lem6  9791  acncc  9851  pwfseqlem3  10071  pwxpndom2  10076  ramval  16334  ramub  16339  ramcl  16355  prmgaplem7  16383  prmgaplem8  16384  imasdsval2  16781  funcf2  17130  funcpropd  17162  funcestrcsetclem8  17389  funcestrcsetclem9  17390  funcsetcestrclem8  17404  funcsetcestrclem9  17405  fsfnn0gsumfsffz  19096  gsummptnn0fzfv  19100  frlmfibas  20451  frlmbas3  20465  frlmipval  20468  frlmphllem  20469  frlmphl  20470  elfilspd  20492  islindf4  20527  mplbas2  20710  ltbwe  20712  psr1baslem  20814  psr1basf  20830  fvcoe1  20836  coe1mul2lem1  20896  ply1coe  20925  mamures  20997  mndvcl  20998  mndvass  20999  mndvlid  21000  mndvrid  21001  grpvlinv  21002  grpvrinv  21003  mhmvlin  21004  mamucl  21006  mamuass  21007  mamudi  21008  mamudir  21009  mamuvs1  21010  mamuvs2  21011  mamulid  21046  mamurid  21047  mattposcl  21058  mattpostpos  21059  tposmap  21062  mamutpos  21063  matgsumcl  21065  mavmulcl  21152  mavmulass  21154  mavmulsolcl  21156  marepvcl  21174  1marepvmarrepid  21180  mdetleib2  21193  mdetf  21200  mdetdiaglem  21203  mdetrlin  21207  mdetrsca  21208  mdetralt  21213  mdetunilem7  21223  mdetunilem9  21225  maducoeval2  21245  madutpos  21247  madugsum  21248  madurid  21249  cramerimplem1  21288  m2pmfzmap  21352  decpmatval  21370  pmatcollpw3lem  21388  pmatcollpw3fi1lem1  21391  pmatcollpw3fi1lem2  21392  pm2mp  21430  chfacfisf  21459  chfacfisfcpmat  21460  chfacfscmulgsum  21465  chfacfpmmulgsum  21469  chfacfpmmulgsum2  21470  cayhamlem1  21471  cpmadugsumlemF  21481  cpmadugsumfi  21482  cayhamlem2  21489  chcoeffeqlem  21490  cayleyhamilton1  21497  pnrmopn  21948  xkoptsub  22259  xkopt  22260  tmdgsum  22700  imasdsf1olem  22980  rrxnm  23995  rrxds  23997  rrxf  24005  rrxmvallem  24008  rrxbasefi  24014  rrxdsfi  24015  ehlbase  24019  ovolscalem2  24118  uniioombl  24193  tdeglem2  24662  plypf1  24809  ulmclm  24982  ulmcaulem  24989  ulmcau  24990  ulmss  24992  ulmbdd  24993  ulmcn  24994  ulmdvlem1  24995  ulmdvlem2  24996  ulmdvlem3  24997  mtest  24999  mtestbdd  25000  mbfulm  25001  iblulm  25002  itgulm  25003  itgulm2  25004  adjval2  29674  fmptco1f1o  30392  fcobijfs  30485  resf1o  30492  fpwrelmap  30495  fply1  30982  elrspunidl  31014  fedgmullem1  31113  fedgmul  31115  extdg1id  31141  smatrcl  31149  mbfmf  31623  elmbfmvol2  31635  eulerpartlemelr  31725  eulerpartlemf  31738  eulerpartlemt  31739  eulerpartgbij  31740  eulerpartlemgu  31745  eulerpartlemgh  31746  eulerpartlemgf  31747  eulerpartlemgs2  31748  reprf  31993  reprsuc  31996  vtsprod  32020  circlemethhgt  32024  tgoldbachgtd  32043  satfv1lem  32722  satfvel  32772  satefvfmla0  32778  satefvfmla1  32785  prv1n  32791  mrsubff1  32874  mrsub0  32876  mrsubf  32877  mrsubccat  32878  mrsubcn  32879  msubrn  32889  msubff  32890  msubf  32892  msubff1  32916  mclsind  32930  uncf  35036  curunc  35039  unccur  35040  matunitlindflem1  35053  matunitlindflem2  35054  poimirlem4  35061  poimirlem5  35062  poimirlem6  35063  poimirlem7  35064  poimirlem8  35065  poimirlem10  35067  poimirlem11  35068  poimirlem12  35069  poimirlem16  35073  poimirlem17  35074  poimirlem18  35075  poimirlem19  35076  poimirlem20  35077  poimirlem21  35078  poimirlem22  35079  poimirlem25  35082  poimirlem26  35083  poimirlem27  35084  poimirlem29  35086  poimirlem30  35087  poimirlem31  35088  poimirlem32  35089  poimir  35090  broucube  35091  mblfinlem3  35096  mblfinlem4  35097  ismblfin  35098  rrnmet  35267  rrndstprj1  35268  rrndstprj2  35269  rrncmslem  35270  rrnequiv  35273  fsuppind  39456  mapco2g  39655  mapfzcons1  39658  mapfzcons2  39660  mzpcompact2lem  39692  eldiophb  39698  elmapresaunres2  39712  eq0rabdioph  39717  rexrabdioph  39735  eldioph4b  39752  diophren  39754  rmydioph  39955  rmxdioph  39957  expdiophlem2  39963  expdioph  39964  pw2f1o2val2  39981  wepwsolem  39986  pwfi2f1o  40040  rfovcnvf1od  40705  rfovcnvfvd  40708  fsovrfovd  40710  fsovcnvlem  40714  ntrk0kbimka  40742  neik0pk1imk0  40750  ntrclsfveq1  40763  ntrclsfveq2  40764  ntrclsfveq  40765  ntrclsss  40766  ntrclsiso  40770  ntrclsk2  40771  ntrclskb  40772  ntrclsk3  40773  ntrclsk13  40774  ntrclsk4  40775  ntrneifv3  40785  ntrneineine0lem  40786  ntrneineine1lem  40787  ntrneifv4  40788  ntrneiel2  40789  ntrneicls00  40792  ntrneicls11  40793  ntrneiiso  40794  ntrneik2  40795  ntrneikb  40797  ntrneixb  40798  ntrneik3  40799  ntrneix3  40800  ntrneik13  40801  ntrneix13  40802  ntrneik4w  40803  ntrneik4  40804  clsneifv3  40813  clsneifv4  40814  neicvgfv  40824  k0004ss2  40855  k0004val0  40857  mnringbasefd  40926  mnugrud  40992  mapss2  41834  difmap  41836  inmap  41838  difmapsn  41841  ssmapsn  41845  mccllem  42239  dvnprodlem1  42588  dvnprodlem2  42589  fourierdlem11  42760  fourierdlem12  42761  fourierdlem13  42762  fourierdlem14  42763  fourierdlem34  42783  fourierdlem41  42790  fourierdlem48  42796  fourierdlem49  42797  fourierdlem54  42802  fourierdlem63  42811  fourierdlem64  42812  fourierdlem65  42813  fourierdlem69  42817  fourierdlem72  42820  fourierdlem74  42822  fourierdlem75  42823  fourierdlem79  42827  fourierdlem85  42833  fourierdlem88  42836  fourierdlem89  42837  fourierdlem90  42838  fourierdlem91  42839  fourierdlem92  42840  fourierdlem94  42842  fourierdlem97  42845  fourierdlem103  42851  fourierdlem104  42852  fourierdlem111  42859  fourierdlem113  42861  etransclem24  42900  etransclem26  42902  etransclem27  42903  etransclem28  42904  etransclem31  42907  etransclem32  42908  etransclem33  42909  etransclem34  42910  etransclem35  42911  etransclem37  42913  etransclem38  42914  rrxtopnfi  42929  rrndistlt  42932  qndenserrnbllem  42936  rrxsnicc  42942  ioorrnopnlem  42946  subsaliuncl  42998  hoicvr  43187  ovnprodcl  43193  ovnsupge0  43196  ovnlecvr  43197  ovncvrrp  43203  ovn0lem  43204  ovnsubaddlem1  43209  sge0hsphoire  43228  hoidmv1le  43233  hoidmvlelem1  43234  hoidmvlelem2  43235  hoidmvlelem3  43236  hoidmvlelem4  43237  hoidmvlelem5  43238  hoidmvle  43239  ovnhoilem2  43241  ovnlecvr2  43249  ovncvr2  43250  hoiqssbllem1  43261  hoiqssbllem2  43262  hoiqssbllem3  43263  hspmbllem2  43266  opnvonmbllem2  43272  ovolval2lem  43282  ovolval2  43283  ovolval3  43286  ovolval4lem2  43289  ovolval5lem3  43293  ovnovollem1  43295  ovnovollem2  43296  vonvolmbllem  43299  vonvolmbl2  43302  vonvol2  43303  snvonmbl  43325  vonsn  43330  iccpartxr  43936  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  intop  44463  assintop  44469  isassintop  44470  ofaddmndmap  44745  rmsupp0  44770  domnmsuppn0  44771  rmsuppss  44772  mndpsuppss  44773  scmsuppss  44774  gsumlsscl  44785  lincfsuppcl  44822  linccl  44823  lcosn0  44829  lincdifsn  44833  lincsum  44838  lincscm  44839  lincscmcl  44841  islinindfis  44858  lincext1  44863  lincext2  44864  lincext3  44865  lindslinindimp2lem1  44867  lindslinindimp2lem2  44868  lindslinindimp2lem4  44870  lindslinindsimp2lem5  44871  snlindsntor  44880  lincresunitlem2  44885  lincresunit3lem1  44888  lincresunit3lem2  44889  lincresunit3  44890  lincreslvec3  44891  isldepslvec2  44894  zlmodzxzldeplem2  44910  zlmodzxzldeplem3  44911  ldepsnlinclem1  44914  ldepsnlinclem2  44915  1arymaptf1  45056  1arymaptfo  45057  2arympt  45063  2arymaptf1  45067  2arymaptfo  45068  prelrrx2b  45128  eenglngeehlnmlem1  45151  eenglngeehlnmlem2  45152  aacllem  45329