Theorem elmap 8909

Description: Membership relation for set exponentiation. (Contributed by NM, 8-Dec-2003.)

Hypotheses

Ref	Expression
elmap.1	⊢ 𝐴 ∈ V
elmap.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
elmap	⊢ (𝐹 ∈ (𝐴 ↑m 𝐵) ↔ 𝐹:𝐵⟶𝐴)

Proof of Theorem elmap

Step	Hyp	Ref	Expression
1		elmap.1	. 2 ⊢ 𝐴 ∈ V
2		elmap.2	. 2 ⊢ 𝐵 ∈ V
3		elmapg 8877	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐹 ∈ (𝐴 ↑m 𝐵) ↔ 𝐹:𝐵⟶𝐴))
4	1, 2, 3	mp2an 692	1 ⊢ (𝐹 ∈ (𝐴 ↑m 𝐵) ↔ 𝐹:𝐵⟶𝐴)

Syntax hints:   ↔ wb 206   ∈ wcel 2105  Vcvv 3477  ⟶wf 6558  (class class class)co 7430   ↑_m cmap 8864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-map 8866

This theorem is referenced by:  mapval2  8910  fvmptmap  8919  mapsnconst  8930  mapsncnv  8931  xpmapenlem  9182  pwfseqlem3  10697  tskcard  10818  ingru  10852  rpnnen1lem1  13017  rpnnen1lem3  13018  rpnnen1lem4  13019  rpnnen1lem5  13020  facmapnn  14320  prmreclem2  16950  1arith  16960  vdwlem6  17019  vdwlem7  17020  vdwlem8  17021  vdwlem9  17022  vdwlem11  17024  vdwlem13  17026  prmgapprmo  17095  isfunc  17914  isfuncd  17915  idfucl  17931  cofucl  17938  funcres2b  17947  wunfunc  17951  wunfuncOLD  17952  catcfuccl  18172  catcfucclOLD  18173  funcestrcsetclem9  18203  ismgmhm  18721  ismhm  18810  efmnd1bas  18918  smndex1ibas  18925  smndex1gbas  18927  dfrhm2  20490  isabv  20828  pjdm  21744  pjfval2  21746  psrelbas  21971  psraddcl  21975  psraddclOLD  21976  psrmulcllem  21982  psrvscacl  21988  psr0cl  21989  psrnegcl  21991  psr1cl  21998  subrgpsr  22015  mvrf  22022  mplmon  22070  mplcoe1  22072  coe1fval3  22225  00ply1bas  22256  ply1plusgfvi  22258  coe1z  22281  coe1mul2  22287  coe1tm  22291  pnrmopn  23366  distgp  24122  indistgp  24123  ehl1eudis  25467  ehl2eudis  25469  elovolmlem  25522  itg2seq  25791  coeeulem  26277  coeeq  26280  aannenlem1  26384  dvntaylp  26427  taylthlem1  26429  taylthlem2  26430  taylthlem2OLD  26431  pserdvlem2  26486  lgamgulmlem6  27091  sqff1o  27239  isismt  28556  elee  28923  islno  30781  nmooval  30791  ajfval  30837  h2hcau  31007  h2hlm  31008  hcau  31212  hlimadd  31221  hhcms  31231  hlim0  31263  hhsscms  31306  pjmf1  31744  hosmval  31763  hommval  31764  hodmval  31765  hfsmval  31766  hfmmval  31767  elcnop  31885  ellnop  31886  elhmop  31901  hmopex  31903  nlfnval  31909  elcnfn  31910  ellnfn  31911  dmadjss  31915  dmadjop  31916  adjeu  31917  adjval  31918  hhcno  31932  hhcnf  31933  adjbdln  32111  isst  32241  ishst  32242  maprnin  32748  fpwrelmap  32750  fpwrelmapffs  32751  ismnt  32957  mgcval  32961  fply1  33563  zarcmplem  33841  eulerpartleme  34344  eulerpartlemt  34352  eulerpartlemr  34355  eulerpartlemmf  34356  eulerpartlemgvv  34357  eulerpartlemgs2  34361  eulerpartlemn  34362  reprinfz1  34615  breprexplemb  34624  breprexpnat  34627  vtsval  34630  circlemethnat  34634  circlemethhgt  34636  ex-sategoelel12  35411  mrsubff  35496  mrsubrn  35497  msubff  35514  poimirlem3  37609  poimirlem4  37610  poimirlem17  37623  poimirlem20  37626  poimirlem24  37630  poimirlem25  37631  poimirlem29  37635  poimirlem30  37636  poimirlem31  37637  poimirlem32  37638  isrngohom  37951  islfl  39041  islpolN  41465  constmap  42700  mzpclall  42714  mzpf  42723  mzpindd  42733  mzpcompact2lem  42738  eldiophb  42744  mendring  43176  clsk1independent  44035  k0004lem3  44138  mnringmulrcld  44223  dvnprodlem3  45903  fourierdlem70  46131  fourierdlem102  46163  fourierdlem114  46175  etransclem35  46224  hoicvrrex  46511  ovnhoilem1  46556  ovnovollem2  46612  nnsum3primes4  47712  nnsum3primesprm  47714  grimfn  47802  isgrim  47805  rrx2xpref1o  48567  rrx2linesl  48592  line2  48601  line2x  48603  line2y  48604  funcf2lem  48810  aacllem  49031