Theorem elmap 8929

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

Syntax hints:   ↔ wb 206   ∈ wcel 2108  Vcvv 3488  ⟶wf 6569  (class class class)co 7448   ↑_m cmap 8884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-map 8886

This theorem is referenced by:  mapval2  8930  fvmptmap  8939  mapsnconst  8950  mapsncnv  8951  xpmapenlem  9210  pwfseqlem3  10729  tskcard  10850  ingru  10884  rpnnen1lem1  13043  rpnnen1lem3  13044  rpnnen1lem4  13045  rpnnen1lem5  13046  facmapnn  14334  prmreclem2  16964  1arith  16974  vdwlem6  17033  vdwlem7  17034  vdwlem8  17035  vdwlem9  17036  vdwlem11  17038  vdwlem13  17040  prmgapprmo  17109  isfunc  17928  isfuncd  17929  idfucl  17945  cofucl  17952  funcres2b  17961  wunfunc  17965  wunfuncOLD  17966  catcfuccl  18186  catcfucclOLD  18187  funcestrcsetclem9  18217  ismgmhm  18734  ismhm  18820  efmnd1bas  18928  smndex1ibas  18935  smndex1gbas  18937  dfrhm2  20500  isabv  20834  pjdm  21750  pjfval2  21752  psrelbas  21977  psraddcl  21981  psraddclOLD  21982  psrmulcllem  21988  psrvscacl  21994  psr0cl  21995  psrnegcl  21997  psr1cl  22004  subrgpsr  22021  mvrf  22028  mplmon  22076  mplcoe1  22078  coe1fval3  22231  00ply1bas  22262  ply1plusgfvi  22264  coe1z  22287  coe1mul2  22293  coe1tm  22297  pnrmopn  23372  distgp  24128  indistgp  24129  ehl1eudis  25473  ehl2eudis  25475  elovolmlem  25528  itg2seq  25797  coeeulem  26283  coeeq  26286  aannenlem1  26388  dvntaylp  26431  taylthlem1  26433  taylthlem2  26434  taylthlem2OLD  26435  pserdvlem2  26490  lgamgulmlem6  27095  sqff1o  27243  isismt  28560  elee  28927  islno  30785  nmooval  30795  ajfval  30841  h2hcau  31011  h2hlm  31012  hcau  31216  hlimadd  31225  hhcms  31235  hlim0  31267  hhsscms  31310  pjmf1  31748  hosmval  31767  hommval  31768  hodmval  31769  hfsmval  31770  hfmmval  31771  elcnop  31889  ellnop  31890  elhmop  31905  hmopex  31907  nlfnval  31913  elcnfn  31914  ellnfn  31915  dmadjss  31919  dmadjop  31920  adjeu  31921  adjval  31922  hhcno  31936  hhcnf  31937  adjbdln  32115  isst  32245  ishst  32246  maprnin  32745  fpwrelmap  32747  fpwrelmapffs  32748  ismnt  32956  mgcval  32960  fply1  33549  zarcmplem  33827  eulerpartleme  34328  eulerpartlemt  34336  eulerpartlemr  34339  eulerpartlemmf  34340  eulerpartlemgvv  34341  eulerpartlemgs2  34345  eulerpartlemn  34346  reprinfz1  34599  breprexplemb  34608  breprexpnat  34611  vtsval  34614  circlemethnat  34618  circlemethhgt  34620  ex-sategoelel12  35395  mrsubff  35480  mrsubrn  35481  msubff  35498  poimirlem3  37583  poimirlem4  37584  poimirlem17  37597  poimirlem20  37600  poimirlem24  37604  poimirlem25  37605  poimirlem29  37609  poimirlem30  37610  poimirlem31  37611  poimirlem32  37612  isrngohom  37925  islfl  39016  islpolN  41440  constmap  42669  mzpclall  42683  mzpf  42692  mzpindd  42702  mzpcompact2lem  42707  eldiophb  42713  mendring  43149  clsk1independent  44008  k0004lem3  44111  mnringmulrcld  44197  dvnprodlem3  45869  fourierdlem70  46097  fourierdlem102  46129  fourierdlem114  46141  etransclem35  46190  hoicvrrex  46477  ovnhoilem1  46522  ovnovollem2  46578  nnsum3primes4  47662  nnsum3primesprm  47664  grimfn  47749  isgrim  47752  rrx2xpref1o  48452  rrx2linesl  48477  line2  48486  line2x  48488  line2y  48489  funcf2lem  48685  aacllem  48895