Theorem elmap 8813

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

Syntax hints:   ↔ wb 208   ∈ wcel 2121  Vcvv 3433  ⟶wf 6484  (class class class)co 7359   ↑_m cmap 8767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5220  ax-pow 5296  ax-pr 5364  ax-un 7681

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-sbc 3725  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-opab 5137  df-id 5515  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-fv 6496  df-ov 7362  df-oprab 7363  df-mpo 7364  df-map 8769

This theorem is referenced by:  mapval2  8814  fvmptmap  8823  mapsnconst  8834  mapsncnv  8835  xpmapenlem  9076  pwfseqlem3  10579  tskcard  10700  ingru  10734  rpnnen1lem1  12923  rpnnen1lem3  12924  rpnnen1lem4  12925  rpnnen1lem5  12926  facmapnn  14242  prmreclem2  16883  1arith  16893  vdwlem6  16952  vdwlem7  16953  vdwlem8  16954  vdwlem9  16955  vdwlem11  16957  vdwlem13  16959  prmgapprmo  17028  isfunc  17826  isfuncd  17827  idfucl  17843  cofucl  17850  funcres2b  17859  wunfunc  17863  catcfuccl  18080  funcestrcsetclem9  18109  ismgmhm  18659  ismhm  18748  efmnd1bas  18856  smndex1ibas  18863  smndex1gbas  18865  smndex1gbasOLD  18866  dfrhm2  20448  isabv  20786  pjdm  21685  pjfval2  21687  psrelbas  21913  psraddcl  21917  psrmulcllem  21923  psrvscacl  21929  psr0cl  21930  psrnegcl  21932  psr1cl  21938  subrgpsr  21955  mvrf  21962  mplmon  22014  mplcoe1  22016  coe1fval3  22196  00ply1bas  22227  ply1plusgfvi  22229  coe1z  22252  coe1mul2  22258  coe1tm  22262  pnrmopn  23329  distgp  24085  indistgp  24086  ehl1eudis  25408  ehl2eudis  25410  elovolmlem  25462  itg2seq  25730  coeeulem  26210  coeeq  26213  aannenlem1  26315  dvntaylp  26357  taylthlem1  26359  taylthlem2  26360  pserdvlem2  26414  lgamgulmlem6  27018  sqff1o  27166  isismt  28622  elee  28982  islno  30844  nmooval  30854  ajfval  30900  h2hcau  31070  h2hlm  31071  hcau  31275  hlimadd  31284  hhcms  31294  hlim0  31326  hhsscms  31369  pjmf1  31807  hosmval  31826  hommval  31827  hodmval  31828  hfsmval  31829  hfmmval  31830  elcnop  31948  ellnop  31949  elhmop  31964  hmopex  31966  nlfnval  31972  elcnfn  31973  ellnfn  31974  dmadjss  31978  dmadjop  31979  adjeu  31980  adjval  31981  hhcno  31995  hhcnf  31996  adjbdln  32174  isst  32304  ishst  32305  maprnin  32825  fpwrelmap  32827  fpwrelmapffs  32828  ismnt  33064  mgcval  33068  fply1  33651  psrmon  33743  zarcmplem  34075  eulerpartleme  34557  eulerpartlemt  34565  eulerpartlemr  34568  eulerpartlemmf  34569  eulerpartlemgvv  34570  eulerpartlemgs2  34574  eulerpartlemn  34575  reprinfz1  34816  breprexplemb  34825  breprexpnat  34828  vtsval  34831  circlemethnat  34835  circlemethhgt  34837  ex-sategoelel12  35668  mrsubff  35753  mrsubrn  35754  msubff  35771  poimirlem3  38003  poimirlem4  38004  poimirlem17  38017  poimirlem20  38020  poimirlem24  38024  poimirlem25  38025  poimirlem29  38029  poimirlem30  38030  poimirlem31  38031  poimirlem32  38032  isrngohom  38345  islfl  39565  islpolN  41988  constmap  43175  mzpclall  43189  mzpf  43198  mzpindd  43208  mzpcompact2lem  43213  eldiophb  43219  mendring  43646  clsk1independent  44503  k0004lem3  44606  mnringmulrcld  44685  dvnprodlem3  46403  fourierdlem70  46631  fourierdlem102  46663  fourierdlem114  46675  etransclem35  46724  hoicvrrex  47011  ovnhoilem1  47056  ovnovollem2  47112  nnsum3primes4  48291  nnsum3primesprm  48293  grimfn  48382  isgrim  48385  rrx2xpref1o  49221  rrx2linesl  49246  line2  49255  line2x  49257  line2y  49258  funcf2lem  49583  aacllem  50303