Theorem elmap 8809

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 8776	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐹 ∈ (𝐴 ↑m 𝐵) ↔ 𝐹:𝐵⟶𝐴))
4	1, 2, 3	mp2an 692	1 ⊢ (𝐹 ∈ (𝐴 ↑m 𝐵) ↔ 𝐹:𝐵⟶𝐴)

Syntax hints:   ↔ wb 206   ∈ wcel 2113  Vcvv 3440  ⟶wf 6488  (class class class)co 7358   ↑_m cmap 8763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7361  df-oprab 7362  df-mpo 7363  df-map 8765

This theorem is referenced by:  mapval2  8810  fvmptmap  8819  mapsnconst  8830  mapsncnv  8831  xpmapenlem  9072  pwfseqlem3  10571  tskcard  10692  ingru  10726  rpnnen1lem1  12891  rpnnen1lem3  12892  rpnnen1lem4  12893  rpnnen1lem5  12894  facmapnn  14208  prmreclem2  16845  1arith  16855  vdwlem6  16914  vdwlem7  16915  vdwlem8  16916  vdwlem9  16917  vdwlem11  16919  vdwlem13  16921  prmgapprmo  16990  isfunc  17788  isfuncd  17789  idfucl  17805  cofucl  17812  funcres2b  17821  wunfunc  17825  catcfuccl  18042  funcestrcsetclem9  18071  ismgmhm  18621  ismhm  18710  efmnd1bas  18818  smndex1ibas  18825  smndex1gbas  18827  dfrhm2  20410  isabv  20744  pjdm  21662  pjfval2  21664  psrelbas  21890  psraddcl  21894  psraddclOLD  21895  psrmulcllem  21901  psrvscacl  21907  psr0cl  21908  psrnegcl  21910  psr1cl  21916  subrgpsr  21933  mvrf  21940  mplmon  21990  mplcoe1  21992  coe1fval3  22149  00ply1bas  22180  ply1plusgfvi  22182  coe1z  22205  coe1mul2  22211  coe1tm  22215  pnrmopn  23287  distgp  24043  indistgp  24044  ehl1eudis  25376  ehl2eudis  25378  elovolmlem  25431  itg2seq  25699  coeeulem  26185  coeeq  26188  aannenlem1  26292  dvntaylp  26335  taylthlem1  26337  taylthlem2  26338  taylthlem2OLD  26339  pserdvlem2  26394  lgamgulmlem6  27000  sqff1o  27148  isismt  28606  elee  28966  islno  30828  nmooval  30838  ajfval  30884  h2hcau  31054  h2hlm  31055  hcau  31259  hlimadd  31268  hhcms  31278  hlim0  31310  hhsscms  31353  pjmf1  31791  hosmval  31810  hommval  31811  hodmval  31812  hfsmval  31813  hfmmval  31814  elcnop  31932  ellnop  31933  elhmop  31948  hmopex  31950  nlfnval  31956  elcnfn  31957  ellnfn  31958  dmadjss  31962  dmadjop  31963  adjeu  31964  adjval  31965  hhcno  31979  hhcnf  31980  adjbdln  32158  isst  32288  ishst  32289  maprnin  32810  fpwrelmap  32812  fpwrelmapffs  32813  ismnt  33065  mgcval  33069  fply1  33639  zarcmplem  34038  eulerpartleme  34520  eulerpartlemt  34528  eulerpartlemr  34531  eulerpartlemmf  34532  eulerpartlemgvv  34533  eulerpartlemgs2  34537  eulerpartlemn  34538  reprinfz1  34779  breprexplemb  34788  breprexpnat  34791  vtsval  34794  circlemethnat  34798  circlemethhgt  34800  ex-sategoelel12  35621  mrsubff  35706  mrsubrn  35707  msubff  35724  poimirlem3  37820  poimirlem4  37821  poimirlem17  37834  poimirlem20  37837  poimirlem24  37841  poimirlem25  37842  poimirlem29  37846  poimirlem30  37847  poimirlem31  37848  poimirlem32  37849  isrngohom  38162  islfl  39316  islpolN  41739  constmap  42951  mzpclall  42965  mzpf  42974  mzpindd  42984  mzpcompact2lem  42989  eldiophb  42995  mendring  43426  clsk1independent  44283  k0004lem3  44386  mnringmulrcld  44465  dvnprodlem3  46188  fourierdlem70  46416  fourierdlem102  46448  fourierdlem114  46460  etransclem35  46509  hoicvrrex  46796  ovnhoilem1  46841  ovnovollem2  46897  nnsum3primes4  48030  nnsum3primesprm  48032  grimfn  48121  isgrim  48124  rrx2xpref1o  48960  rrx2linesl  48985  line2  48994  line2x  48996  line2y  48997  funcf2lem  49322  aacllem  50042