Theorem elmap 8795

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

Syntax hints:   ↔ wb 206   ∈ wcel 2111  Vcvv 3436  ⟶wf 6477  (class class class)co 7346   ↑_m cmap 8750

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3742  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-fv 6489  df-ov 7349  df-oprab 7350  df-mpo 7351  df-map 8752

This theorem is referenced by:  mapval2  8796  fvmptmap  8805  mapsnconst  8816  mapsncnv  8817  xpmapenlem  9057  pwfseqlem3  10548  tskcard  10669  ingru  10703  rpnnen1lem1  12873  rpnnen1lem3  12874  rpnnen1lem4  12875  rpnnen1lem5  12876  facmapnn  14189  prmreclem2  16826  1arith  16836  vdwlem6  16895  vdwlem7  16896  vdwlem8  16897  vdwlem9  16898  vdwlem11  16900  vdwlem13  16902  prmgapprmo  16971  isfunc  17768  isfuncd  17769  idfucl  17785  cofucl  17792  funcres2b  17801  wunfunc  17805  catcfuccl  18022  funcestrcsetclem9  18051  ismgmhm  18601  ismhm  18690  efmnd1bas  18798  smndex1ibas  18805  smndex1gbas  18807  dfrhm2  20390  isabv  20724  pjdm  21642  pjfval2  21644  psrelbas  21869  psraddcl  21873  psraddclOLD  21874  psrmulcllem  21880  psrvscacl  21886  psr0cl  21887  psrnegcl  21889  psr1cl  21896  subrgpsr  21913  mvrf  21920  mplmon  21968  mplcoe1  21970  coe1fval3  22119  00ply1bas  22150  ply1plusgfvi  22152  coe1z  22175  coe1mul2  22181  coe1tm  22185  pnrmopn  23256  distgp  24012  indistgp  24013  ehl1eudis  25345  ehl2eudis  25347  elovolmlem  25400  itg2seq  25668  coeeulem  26154  coeeq  26157  aannenlem1  26261  dvntaylp  26304  taylthlem1  26306  taylthlem2  26307  taylthlem2OLD  26308  pserdvlem2  26363  lgamgulmlem6  26969  sqff1o  27117  isismt  28510  elee  28870  islno  30728  nmooval  30738  ajfval  30784  h2hcau  30954  h2hlm  30955  hcau  31159  hlimadd  31168  hhcms  31178  hlim0  31210  hhsscms  31253  pjmf1  31691  hosmval  31710  hommval  31711  hodmval  31712  hfsmval  31713  hfmmval  31714  elcnop  31832  ellnop  31833  elhmop  31848  hmopex  31850  nlfnval  31856  elcnfn  31857  ellnfn  31858  dmadjss  31862  dmadjop  31863  adjeu  31864  adjval  31865  hhcno  31879  hhcnf  31880  adjbdln  32058  isst  32188  ishst  32189  maprnin  32709  fpwrelmap  32711  fpwrelmapffs  32712  ismnt  32959  mgcval  32963  fply1  33516  zarcmplem  33889  eulerpartleme  34371  eulerpartlemt  34379  eulerpartlemr  34382  eulerpartlemmf  34383  eulerpartlemgvv  34384  eulerpartlemgs2  34388  eulerpartlemn  34389  reprinfz1  34630  breprexplemb  34639  breprexpnat  34642  vtsval  34645  circlemethnat  34649  circlemethhgt  34651  ex-sategoelel12  35459  mrsubff  35544  mrsubrn  35545  msubff  35562  poimirlem3  37662  poimirlem4  37663  poimirlem17  37676  poimirlem20  37679  poimirlem24  37683  poimirlem25  37684  poimirlem29  37688  poimirlem30  37689  poimirlem31  37690  poimirlem32  37691  isrngohom  38004  islfl  39098  islpolN  41521  constmap  42745  mzpclall  42759  mzpf  42768  mzpindd  42778  mzpcompact2lem  42783  eldiophb  42789  mendring  43220  clsk1independent  44078  k0004lem3  44181  mnringmulrcld  44260  dvnprodlem3  45985  fourierdlem70  46213  fourierdlem102  46245  fourierdlem114  46257  etransclem35  46306  hoicvrrex  46593  ovnhoilem1  46638  ovnovollem2  46694  nnsum3primes4  47818  nnsum3primesprm  47820  grimfn  47909  isgrim  47912  rrx2xpref1o  48749  rrx2linesl  48774  line2  48783  line2x  48785  line2y  48786  funcf2lem  49112  aacllem  49832