Theorem elmap 8864

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

Syntax hints:   ↔ wb 205   ∈ wcel 2106  Vcvv 3474  ⟶wf 6539  (class class class)co 7408   ↑_m cmap 8819

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7411  df-oprab 7412  df-mpo 7413  df-map 8821

This theorem is referenced by:  mapval2  8865  fvmptmap  8874  mapsnconst  8885  mapsncnv  8886  xpmapenlem  9143  pwfseqlem3  10654  tskcard  10775  ingru  10809  rpnnen1lem1  12961  rpnnen1lem3  12962  rpnnen1lem4  12963  rpnnen1lem5  12964  facmapnn  14244  prmreclem2  16849  1arith  16859  vdwlem6  16918  vdwlem7  16919  vdwlem8  16920  vdwlem9  16921  vdwlem11  16923  vdwlem13  16925  prmgapprmo  16994  isfunc  17813  isfuncd  17814  idfucl  17830  cofucl  17837  funcres2b  17846  wunfunc  17848  wunfuncOLD  17849  catcfuccl  18068  catcfucclOLD  18069  funcestrcsetclem9  18099  ismhm  18672  efmnd1bas  18773  smndex1ibas  18780  smndex1gbas  18782  dfrhm2  20252  isabv  20426  pjdm  21261  pjfval2  21263  psrelbas  21497  psraddcl  21501  psrmulcllem  21505  psrvscacl  21511  psr0cl  21512  psrnegcl  21514  psr1cl  21521  subrgpsr  21538  mvrf  21543  mplmon  21589  mplcoe1  21591  coe1fval3  21731  00ply1bas  21761  ply1plusgfvi  21763  coe1z  21784  coe1mul2  21790  coe1tm  21794  pnrmopn  22846  distgp  23602  indistgp  23603  ehl1eudis  24936  ehl2eudis  24938  elovolmlem  24990  itg2seq  25259  coeeulem  25737  coeeq  25740  aannenlem1  25840  dvntaylp  25882  taylthlem1  25884  taylthlem2  25885  pserdvlem2  25939  lgamgulmlem6  26535  sqff1o  26683  isismt  27782  elee  28149  islno  30001  nmooval  30011  ajfval  30057  h2hcau  30227  h2hlm  30228  hcau  30432  hlimadd  30441  hhcms  30451  hlim0  30483  hhsscms  30526  pjmf1  30964  hosmval  30983  hommval  30984  hodmval  30985  hfsmval  30986  hfmmval  30987  elcnop  31105  ellnop  31106  elhmop  31121  hmopex  31123  nlfnval  31129  elcnfn  31130  ellnfn  31131  dmadjss  31135  dmadjop  31136  adjeu  31137  adjval  31138  hhcno  31152  hhcnf  31153  adjbdln  31331  isst  31461  ishst  31462  maprnin  31951  fpwrelmap  31953  fpwrelmapffs  31954  ismnt  32148  mgcval  32152  fply1  32632  zarcmplem  32856  eulerpartleme  33357  eulerpartlemt  33365  eulerpartlemr  33368  eulerpartlemmf  33369  eulerpartlemgvv  33370  eulerpartlemgs2  33374  eulerpartlemn  33375  reprinfz1  33629  breprexplemb  33638  breprexpnat  33641  vtsval  33644  circlemethnat  33648  circlemethhgt  33650  ex-sategoelel12  34413  mrsubff  34498  mrsubrn  34499  msubff  34516  poimirlem3  36486  poimirlem4  36487  poimirlem17  36500  poimirlem20  36503  poimirlem24  36507  poimirlem25  36508  poimirlem29  36512  poimirlem30  36513  poimirlem31  36514  poimirlem32  36515  isrngohom  36828  islfl  37925  islpolN  40349  constmap  41441  mzpclall  41455  mzpf  41464  mzpindd  41474  mzpcompact2lem  41479  eldiophb  41485  mendring  41924  clsk1independent  42787  k0004lem3  42890  mnringmulrcld  42977  dvnprodlem3  44654  fourierdlem70  44882  fourierdlem102  44914  fourierdlem114  44926  etransclem35  44975  hoicvrrex  45262  ovnhoilem1  45307  ovnovollem2  45363  nnsum3primes4  46446  nnsum3primesprm  46448  ismgmhm  46543  rrx2xpref1o  47394  rrx2linesl  47419  line2  47428  line2x  47430  line2y  47431  funcf2lem  47628  aacllem  47838