Theorem elmap 7772

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	⊢ (𝐹 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐹:𝐵⟶𝐴)

Proof of Theorem elmap

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

Syntax hints:   ↔ wb 195   ∈ wcel 1977  Vcvv 3173  ⟶wf 5800  (class class class)co 6549   ↑_𝑚 cmap 7744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-map 7746

This theorem is referenced by:  mapval2  7773  fvmptmap  7780  mapsn  7785  mapsnconst  7789  mapsncnv  7790  xpmapenlem  8012  pwfseqlem3  9361  tskcard  9482  ingru  9516  rpnnen1lem1  11691  rpnnen1lem3  11692  rpnnen1lem4  11693  rpnnen1lem5  11694  rpnnen1lem1OLD  11697  rpnnen1lem3OLD  11698  rpnnen1lem4OLD  11699  rpnnen1lem5OLD  11700  facmapnn  12934  prmreclem2  15459  1arith  15469  vdwlem6  15528  vdwlem7  15529  vdwlem8  15530  vdwlem9  15531  vdwlem11  15533  vdwlem13  15535  prmgapprmo  15604  isfunc  16347  isfuncd  16348  idfucl  16364  cofucl  16371  funcres2b  16380  wunfunc  16382  catcfuccl  16582  funcestrcsetclem9  16611  ismhm  17160  symgval  17622  dfrhm2  18540  isabv  18642  psrelbas  19200  psraddcl  19204  psrmulcllem  19208  psrvscacl  19214  psr0cl  19215  psrnegcl  19217  psr1cl  19223  subrgpsr  19240  mvrf  19245  mplmon  19284  mplcoe1  19286  coe1fval3  19399  00ply1bas  19431  ply1plusgfvi  19433  coe1z  19454  coe1mul2  19460  coe1tm  19464  pjdm  19870  pjfval2  19872  pnrmopn  20957  distgp  21713  indistgp  21714  elovolm  23050  elovolmr  23051  ovolmge0  23052  ovolgelb  23055  ovolunlem1a  23071  ovolunlem1  23072  ovoliunlem1  23077  ovoliunlem2  23078  ovolshftlem2  23085  ovolicc2  23097  ioombl1  23137  itg2seq  23315  coeeulem  23784  coeeq  23787  aannenlem1  23887  dvntaylp  23929  taylthlem1  23931  taylthlem2  23932  pserdvlem2  23986  lgamgulmlem6  24560  sqff1o  24708  isismt  25229  elee  25574  islno  26992  nmooval  27002  ajfval  27048  h2hcau  27220  h2hlm  27221  hcau  27425  hlimadd  27434  hhcms  27444  hlim0  27476  hhsscms  27520  pjmf1  27959  hosmval  27978  hommval  27979  hodmval  27980  hfsmval  27981  hfmmval  27982  elcnop  28100  ellnop  28101  elhmop  28116  hmopex  28118  nlfnval  28124  elcnfn  28125  ellnfn  28126  dmadjss  28130  dmadjop  28131  adjeu  28132  adjval  28133  hhcno  28147  hhcnf  28148  adjbdln  28326  isst  28456  ishst  28457  maprnin  28894  fpwrelmap  28896  fpwrelmapffs  28897  eulerpartleme  29752  eulerpartlemt  29760  eulerpartlemr  29763  eulerpartlemmf  29764  eulerpartlemgvv  29765  eulerpartlemgs2  29769  eulerpartlemn  29770  mrsubff  30663  mrsubrn  30664  msubff  30681  poimirlem3  32582  poimirlem4  32583  poimirlem17  32596  poimirlem20  32599  poimirlem24  32603  poimirlem25  32604  poimirlem29  32608  poimirlem30  32609  poimirlem31  32610  poimirlem32  32611  isrngohom  32934  islfl  33365  islpolN  35790  constmap  36294  mzpclall  36308  mzpf  36317  mzpindd  36327  mzpcompact2lem  36332  eldiophb  36338  mendring  36781  clsk1independent  37364  k0004lem3  37467  dvnprodlem3  38838  fourierdlem70  39069  fourierdlem102  39101  fourierdlem114  39113  etransclem35  39162  hoicvrrex  39446  ovnhoilem1  39491  ovnovollem2  39547  nnsum3primes4  40204  nnsum3primesprm  40206  ismgmhm  41573  aacllem  42356