Theorem elmapi 8852

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2145  Vcvv 3453  ⟶wf 6533  (class class class)co 7417   ↑_m cmap 8830

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-ov 7420  df-oprab 7421  df-mpo 7422  df-1st 7990  df-2nd 7991  df-map 8832

This theorem is used by:  elmaprd  8853  mapfset  8855  elmapfn  8870  elmapfun  8871  uncf  8874  elmapssres  8877  mapsspm  8887  mapfvd  8890  elmapresaun  8891  map0b  8894  mapss  8900  mapsncnv  8904  ralxpmap  8907  mapen  9143  mapxpen  9145  mapunen  9148  mapfienlem1  9379  mapfienlem2  9380  mapfienlem3  9381  mapfien  9382  wemaplem2  9523  wemappo  9525  wemapsolem  9526  wemapso  9527  wemapso2lem  9528  wemapwe  9680  iunmapdisj  10030  fseqenlem1  10031  fseqenlem2  10032  numacn  10056  finacn  10057  acndom  10058  acndom2  10061  infpwfien  10069  infmap2  10223  fin23lem40  10357  isf32lem12  10370  isf34lem6  10386  acncc  10446  pwfseqlem3  10673  pwxpndom2  10678  s3rex  15025  ramval  17106  ramub  17111  ramcl  17127  prmgaplem7  17155  prmgaplem8  17156  imasdsval2  17608  funcf2  17963  funcpropd  17997  funcestrcsetclem8  18241  funcestrcsetclem9  18242  funcsetcestrclem8  18256  funcsetcestrclem9  18257  mndpsuppss  18878  mndvcl  18911  mndvass  18912  mndvlid  18913  mndvrid  18914  mhmvlin  18915  fsfnn0gsumfsffz  20116  gsummptnn0fzfv  20120  frlmfibas  21981  frlmbas3  21995  frlmipval  21998  frlmphllem  21999  frlmphl  22000  elfilspd  22022  islindf4  22057  psrbagf  22139  mplbas2  22264  ltbwe  22266  evlsvvvallem  22313  evlsvvval  22315  psr1baslem  22416  psr1basf  22432  fvcoe1  22438  coe1mul2lem1  22499  ply1coe  22529  mamures  22625  grpvlinv  22626  grpvrinv  22627  mamucl  22629  mamuass  22630  mamudi  22631  mamudir  22632  mamuvs1  22633  mamuvs2  22634  mamulid  22669  mamurid  22670  mattposcl  22681  mattpostpos  22682  tposmap  22685  mamutpos  22686  matgsumcl  22688  mavmulcl  22775  mavmulass  22777  mavmulsolcl  22779  marepvcl  22797  1marepvmarrepid  22803  mdetleib2  22816  mdetf  22823  mdetdiaglem  22826  mdetrlin  22830  mdetrsca  22831  mdetralt  22836  mdetunilem7  22846  mdetunilem9  22848  maducoeval2  22868  madutpos  22870  madugsum  22871  madurid  22872  matunitlindflem1  22907  matunitlindflem2  22908  cramerimplem1  22914  m2pmfzmap  22978  decpmatval  22996  pmatcollpw3lem  23014  pmatcollpw3fi1lem1  23017  pmatcollpw3fi1lem2  23018  pm2mp  23056  chfacfisf  23085  chfacfisfcpmat  23086  chfacfscmulgsum  23091  chfacfpmmulgsum  23095  chfacfpmmulgsum2  23096  cayhamlem1  23097  cpmadugsumlemF  23107  cpmadugsumfi  23108  cayhamlem2  23115  chcoeffeqlem  23116  cayleyhamilton1  23123  pnrmopn  23574  xkoptsub  23886  xkopt  23887  tmdgsum  24327  imasdsf1olem  24605  rrxnm  25625  rrxds  25627  rrxf  25635  rrxmvallem  25638  rrxbasefi  25644  rrxdsfi  25645  ehlbase  25649  ovolscalem2  25748  uniioombl  25823  tdeglem2  26293  plypf1  26445  ulmclm  26630  ulmcaulem  26637  ulmcau  26638  ulmss  26640  ulmbdd  26641  ulmcn  26642  ulmdvlem1  26643  ulmdvlem2  26644  ulmdvlem3  26645  mtest  26647  mtestbdd  26648  mbfulm  26649  iblulm  26650  itgulm  26651  itgulm2  26652  adjval2  32380  fmptco1f1o  33114  fcobijfs  33200  fcobijfs2  33201  resf1o  33209  fpwrelmap  33212  elrspunidl  33864  elrspunsn  33865  1arithidomlem2  33954  1arithidom  33955  fply1  33976  psrbasfsupp  34029  selvply1rhmlemb  34037  ply1degltdimlem  34140  fedgmullem1  34147  fedgmul  34149  extdg1id  34184  smatrcl  34314  mbfmf  34773  elmbfmvol2  34786  eulerpartlemelr  34876  eulerpartlemf  34889  eulerpartlemt  34890  eulerpartgbij  34891  eulerpartlemgu  34896  eulerpartlemgh  34897  eulerpartlemgf  34898  eulerpartlemgs2  34899  reprf  35128  reprsuc  35131  vtsprod  35155  circlemethhgt  35159  tgoldbachgtd  35178  satfv1lem  35949  satfvel  35999  satefvfmla0  36005  satefvfmla1  36012  prv1n  36018  mrsubff1  36101  mrsub0  36103  mrsubf  36104  mrsubccat  36105  mrsubcn  36106  msubrn  36116  msubff  36117  msubf  36119  msubff1  36143  mclsind  36157  curunc  38364  unccur  38365  poimirlem4  38381  poimirlem5  38382  poimirlem6  38383  poimirlem7  38384  poimirlem8  38385  poimirlem10  38387  poimirlem11  38388  poimirlem12  38389  poimirlem16  38393  poimirlem17  38394  poimirlem18  38395  poimirlem19  38396  poimirlem20  38397  poimirlem21  38398  poimirlem22  38399  poimirlem25  38402  poimirlem26  38403  poimirlem27  38404  poimirlem29  38406  poimirlem30  38407  poimirlem31  38408  poimirlem32  38409  poimir  38410  broucube  38411  mblfinlem3  38416  mblfinlem4  38417  ismblfin  38418  rrnmet  38587  rrndstprj1  38588  rrndstprj2  38589  rrncmslem  38590  rrnequiv  38593  aks6d1c2lem4  43001  mapcod  43118  evlselv  43443  fsuppind  43444  mhphf  43451  mapco2g  43567  mapfzcons1  43570  mapfzcons2  43572  mzpcompact2lem  43604  eldiophb  43610  elmapresaunres2  43624  eq0rabdioph  43629  rexrabdioph  43643  eldioph4b  43660  diophren  43662  rmydioph  43863  rmxdioph  43865  expdiophlem2  43871  expdioph  43872  pw2f1o2val2  43889  wepwsolem  43891  pwfi2f1o  43945  ofoafo  44205  ofoaid1  44207  ofoaid2  44208  ofoaass  44209  ofoacom  44210  rfovcnvf1od  44852  rfovcnvfvd  44855  fsovrfovd  44857  fsovcnvlem  44861  ntrk0kbimka  44887  neik0pk1imk0  44895  ntrclsfveq1  44908  ntrclsfveq2  44909  ntrclsfveq  44910  ntrclsss  44911  ntrclsiso  44915  ntrclsk2  44916  ntrclskb  44917  ntrclsk3  44918  ntrclsk13  44919  ntrclsk4  44920  ntrneifv3  44930  ntrneineine0lem  44931  ntrneineine1lem  44932  ntrneifv4  44933  ntrneiel2  44934  ntrneicls00  44937  ntrneicls11  44938  ntrneiiso  44939  ntrneik2  44940  ntrneikb  44942  ntrneixb  44943  ntrneik3  44944  ntrneix3  44945  ntrneik13  44946  ntrneix13  44947  ntrneik4w  44948  ntrneik4  44949  clsneifv3  44958  clsneifv4  44959  neicvgfv  44969  k0004ss2  45000  k0004val0  45002  mnringbasefd  45064  mnugrud  45116  mapss2  46044  difmap  46045  inmap  46047  difmapsn  46050  ssmapsn  46054  mccllem  46435  dvnprodlem1  46782  dvnprodlem2  46783  fourierdlem11  46954  fourierdlem12  46955  fourierdlem13  46956  fourierdlem14  46957  fourierdlem34  46977  fourierdlem41  46984  fourierdlem48  46990  fourierdlem49  46991  fourierdlem54  46996  fourierdlem63  47005  fourierdlem64  47006  fourierdlem65  47007  fourierdlem69  47011  fourierdlem72  47014  fourierdlem74  47016  fourierdlem75  47017  fourierdlem79  47021  fourierdlem85  47027  fourierdlem88  47030  fourierdlem89  47031  fourierdlem90  47032  fourierdlem91  47033  fourierdlem92  47034  fourierdlem94  47036  fourierdlem97  47039  fourierdlem103  47045  fourierdlem104  47046  fourierdlem111  47053  fourierdlem113  47055  etransclem24  47094  etransclem26  47096  etransclem27  47097  etransclem28  47098  etransclem31  47101  etransclem32  47102  etransclem33  47103  etransclem34  47104  etransclem35  47105  etransclem37  47107  etransclem38  47108  rrxtopnfi  47123  rrndistlt  47126  qndenserrnbllem  47130  rrxsnicc  47136  ioorrnopnlem  47140  subsaliuncl  47194  hoicvr  47384  ovnprodcl  47390  ovnsupge0  47393  ovnlecvr  47394  ovncvrrp  47400  ovn0lem  47401  ovnsubaddlem1  47406  sge0hsphoire  47425  hoidmv1le  47430  hoidmvlelem1  47431  hoidmvlelem2  47432  hoidmvlelem3  47433  hoidmvlelem4  47434  hoidmvlelem5  47435  hoidmvle  47436  ovnhoilem2  47438  ovnlecvr2  47446  ovncvr2  47447  hoiqssbllem1  47458  hoiqssbllem2  47459  hoiqssbllem3  47460  hspmbllem2  47463  opnvonmbllem2  47469  ovolval2lem  47479  ovolval2  47480  ovolval3  47483  ovolval4lem2  47486  ovolval5lem3  47490  ovnovollem1  47492  ovnovollem2  47493  vonvolmbllem  47496  vonvolmbl2  47499  vonvol2  47500  snvonmbl  47522  vonsn  47527  tmachlem-agreeprod  47773  tmachlem-tpopen  47777  iccpartxr  48327  nnsum4primeseven  48724  nnsum4primesevenALTV  48725  intop  49126  assintop  49132  isassintop  49133  ofaddmndmap  49281  rmsupp0  49306  domnmsuppn0  49307  rmsuppss  49308  scmsuppss  49309  gsumlsscl  49318  lincfsuppcl  49351  linccl  49352  lcosn0  49358  lincdifsn  49362  lincsum  49367  lincscm  49368  lincscmcl  49370  islinindfis  49387  lincext1  49392  lincext2  49393  lincext3  49394  lindslinindimp2lem1  49396  lindslinindimp2lem2  49397  lindslinindimp2lem4  49399  lindslinindsimp2lem5  49400  snlindsntor  49409  lincresunitlem2  49414  lincresunit3lem1  49417  lincresunit3lem2  49418  lincresunit3  49419  lincreslvec3  49420  isldepslvec2  49423  zlmodzxzldeplem2  49439  zlmodzxzldeplem3  49440  ldepsnlinclem1  49443  ldepsnlinclem2  49444  1arymaptf1  49580  1arymaptfo  49581  2arympt  49587  2arymaptf1  49591  2arymaptfo  49592  prelrrx2b  49652  eenglngeehlnmlem1  49675  eenglngeehlnmlem2  49676  aacllem  50780  rr3fvcl  50787  crosspdotsumlem  50805  crossp3d  50808