Theorem elmap 8668

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

Syntax hints:   ↔ wb 205   ∈ wcel 2107  Vcvv 3433  ⟶wf 6433  (class class class)co 7284   ↑_m cmap 8624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-sbc 3718  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-fv 6445  df-ov 7287  df-oprab 7288  df-mpo 7289  df-map 8626

This theorem is referenced by:  mapval2  8669  fvmptmap  8678  mapsnconst  8689  mapsncnv  8690  xpmapenlem  8940  pwfseqlem3  10425  tskcard  10546  ingru  10580  rpnnen1lem1  12727  rpnnen1lem3  12728  rpnnen1lem4  12729  rpnnen1lem5  12730  facmapnn  14008  prmreclem2  16627  1arith  16637  vdwlem6  16696  vdwlem7  16697  vdwlem8  16698  vdwlem9  16699  vdwlem11  16701  vdwlem13  16703  prmgapprmo  16772  isfunc  17588  isfuncd  17589  idfucl  17605  cofucl  17612  funcres2b  17621  wunfunc  17623  wunfuncOLD  17624  catcfuccl  17843  catcfucclOLD  17844  funcestrcsetclem9  17874  ismhm  18441  efmnd1bas  18541  smndex1ibas  18548  smndex1gbas  18550  dfrhm2  19970  isabv  20088  pjdm  20923  pjfval2  20925  psrelbas  21157  psraddcl  21161  psrmulcllem  21165  psrvscacl  21171  psr0cl  21172  psrnegcl  21174  psr1cl  21180  subrgpsr  21197  mvrf  21202  mplmon  21245  mplcoe1  21247  coe1fval3  21388  00ply1bas  21420  ply1plusgfvi  21422  coe1z  21443  coe1mul2  21449  coe1tm  21453  pnrmopn  22503  distgp  23259  indistgp  23260  ehl1eudis  24593  ehl2eudis  24595  elovolmlem  24647  itg2seq  24916  coeeulem  25394  coeeq  25397  aannenlem1  25497  dvntaylp  25539  taylthlem1  25541  taylthlem2  25542  pserdvlem2  25596  lgamgulmlem6  26192  sqff1o  26340  isismt  26904  elee  27271  islno  29124  nmooval  29134  ajfval  29180  h2hcau  29350  h2hlm  29351  hcau  29555  hlimadd  29564  hhcms  29574  hlim0  29606  hhsscms  29649  pjmf1  30087  hosmval  30106  hommval  30107  hodmval  30108  hfsmval  30109  hfmmval  30110  elcnop  30228  ellnop  30229  elhmop  30244  hmopex  30246  nlfnval  30252  elcnfn  30253  ellnfn  30254  dmadjss  30258  dmadjop  30259  adjeu  30260  adjval  30261  hhcno  30275  hhcnf  30276  adjbdln  30454  isst  30584  ishst  30585  maprnin  31075  fpwrelmap  31077  fpwrelmapffs  31078  ismnt  31270  mgcval  31274  fply1  31676  zarcmplem  31840  eulerpartleme  32339  eulerpartlemt  32347  eulerpartlemr  32350  eulerpartlemmf  32351  eulerpartlemgvv  32352  eulerpartlemgs2  32356  eulerpartlemn  32357  reprinfz1  32611  breprexplemb  32620  breprexpnat  32623  vtsval  32626  circlemethnat  32630  circlemethhgt  32632  ex-sategoelel12  33398  mrsubff  33483  mrsubrn  33484  msubff  33501  poimirlem3  35789  poimirlem4  35790  poimirlem17  35803  poimirlem20  35806  poimirlem24  35810  poimirlem25  35811  poimirlem29  35815  poimirlem30  35816  poimirlem31  35817  poimirlem32  35818  isrngohom  36132  islfl  37081  islpolN  39504  constmap  40542  mzpclall  40556  mzpf  40565  mzpindd  40575  mzpcompact2lem  40580  eldiophb  40586  mendring  41024  clsk1independent  41663  k0004lem3  41766  mnringmulrcld  41853  dvnprodlem3  43496  fourierdlem70  43724  fourierdlem102  43756  fourierdlem114  43768  etransclem35  43817  hoicvrrex  44101  ovnhoilem1  44146  ovnovollem2  44202  nnsum3primes4  45251  nnsum3primesprm  45253  ismgmhm  45348  rrx2xpref1o  46075  rrx2linesl  46100  line2  46109  line2x  46111  line2y  46112  funcf2lem  46310  aacllem  46516