Theorem elmap 8812

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  Vcvv 3430  ⟶wf 6488  (class class class)co 7360   ↑_m cmap 8766

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-pow 5302  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  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 7363  df-oprab 7364  df-mpo 7365  df-map 8768

This theorem is referenced by:  mapval2  8813  fvmptmap  8822  mapsnconst  8833  mapsncnv  8834  xpmapenlem  9075  pwfseqlem3  10574  tskcard  10695  ingru  10729  rpnnen1lem1  12919  rpnnen1lem3  12920  rpnnen1lem4  12921  rpnnen1lem5  12922  facmapnn  14238  prmreclem2  16879  1arith  16889  vdwlem6  16948  vdwlem7  16949  vdwlem8  16950  vdwlem9  16951  vdwlem11  16953  vdwlem13  16955  prmgapprmo  17024  isfunc  17822  isfuncd  17823  idfucl  17839  cofucl  17846  funcres2b  17855  wunfunc  17859  catcfuccl  18076  funcestrcsetclem9  18105  ismgmhm  18655  ismhm  18744  efmnd1bas  18852  smndex1ibas  18859  smndex1gbas  18861  smndex1gbasOLD  18862  dfrhm2  20445  isabv  20779  pjdm  21697  pjfval2  21699  psrelbas  21924  psraddcl  21928  psrmulcllem  21934  psrvscacl  21940  psr0cl  21941  psrnegcl  21943  psr1cl  21949  subrgpsr  21966  mvrf  21973  mplmon  22023  mplcoe1  22025  coe1fval3  22182  00ply1bas  22213  ply1plusgfvi  22215  coe1z  22238  coe1mul2  22244  coe1tm  22248  pnrmopn  23318  distgp  24074  indistgp  24075  ehl1eudis  25397  ehl2eudis  25399  elovolmlem  25451  itg2seq  25719  coeeulem  26199  coeeq  26202  aannenlem1  26305  dvntaylp  26348  taylthlem1  26350  taylthlem2  26351  taylthlem2OLD  26352  pserdvlem2  26406  lgamgulmlem6  27011  sqff1o  27159  isismt  28616  elee  28976  islno  30839  nmooval  30849  ajfval  30895  h2hcau  31065  h2hlm  31066  hcau  31270  hlimadd  31279  hhcms  31289  hlim0  31321  hhsscms  31364  pjmf1  31802  hosmval  31821  hommval  31822  hodmval  31823  hfsmval  31824  hfmmval  31825  elcnop  31943  ellnop  31944  elhmop  31959  hmopex  31961  nlfnval  31967  elcnfn  31968  ellnfn  31969  dmadjss  31973  dmadjop  31974  adjeu  31975  adjval  31976  hhcno  31990  hhcnf  31991  adjbdln  32169  isst  32299  ishst  32300  maprnin  32819  fpwrelmap  32821  fpwrelmapffs  32822  ismnt  33058  mgcval  33062  fply1  33633  psrmon  33708  zarcmplem  34041  eulerpartleme  34523  eulerpartlemt  34531  eulerpartlemr  34534  eulerpartlemmf  34535  eulerpartlemgvv  34536  eulerpartlemgs2  34540  eulerpartlemn  34541  reprinfz1  34782  breprexplemb  34791  breprexpnat  34794  vtsval  34797  circlemethnat  34801  circlemethhgt  34803  ex-sategoelel12  35625  mrsubff  35710  mrsubrn  35711  msubff  35728  poimirlem3  37958  poimirlem4  37959  poimirlem17  37972  poimirlem20  37975  poimirlem24  37979  poimirlem25  37980  poimirlem29  37984  poimirlem30  37985  poimirlem31  37986  poimirlem32  37987  isrngohom  38300  islfl  39520  islpolN  41943  constmap  43159  mzpclall  43173  mzpf  43182  mzpindd  43192  mzpcompact2lem  43197  eldiophb  43203  mendring  43634  clsk1independent  44491  k0004lem3  44594  mnringmulrcld  44673  dvnprodlem3  46394  fourierdlem70  46622  fourierdlem102  46654  fourierdlem114  46666  etransclem35  46715  hoicvrrex  47002  ovnhoilem1  47047  ovnovollem2  47103  nnsum3primes4  48276  nnsum3primesprm  48278  grimfn  48367  isgrim  48370  rrx2xpref1o  49206  rrx2linesl  49231  line2  49240  line2x  49242  line2y  49243  funcf2lem  49568  aacllem  50288