Theorem elmap 8816

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

Syntax hints:   ↔ wb 207   ∈ wcel 2119  Vcvv 3432  ⟶wf 6488  (class class class)co 7363   ↑_m cmap 8770

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7366  df-oprab 7367  df-mpo 7368  df-map 8772

This theorem is referenced by:  mapval2  8817  fvmptmap  8826  mapsnconst  8837  mapsncnv  8838  xpmapenlem  9079  pwfseqlem3  10581  tskcard  10702  ingru  10736  rpnnen1lem1  12926  rpnnen1lem3  12927  rpnnen1lem4  12928  rpnnen1lem5  12929  facmapnn  14245  prmreclem2  16886  1arith  16896  vdwlem6  16955  vdwlem7  16956  vdwlem8  16957  vdwlem9  16958  vdwlem11  16960  vdwlem13  16962  prmgapprmo  17031  isfunc  17829  isfuncd  17830  idfucl  17846  cofucl  17853  funcres2b  17862  wunfunc  17866  catcfuccl  18083  funcestrcsetclem9  18112  ismgmhm  18662  ismhm  18751  efmnd1bas  18859  smndex1ibas  18866  smndex1gbas  18868  smndex1gbasOLD  18869  dfrhm2  20452  isabv  20790  pjdm  21689  pjfval2  21691  psrelbas  21917  psraddcl  21921  psrmulcllem  21927  psrvscacl  21933  psr0cl  21934  psrnegcl  21936  psr1cl  21942  subrgpsr  21959  mvrf  21966  mplmon  22018  mplcoe1  22020  coe1fval3  22200  00ply1bas  22231  ply1plusgfvi  22233  coe1z  22256  coe1mul2  22262  coe1tm  22266  pnrmopn  23333  distgp  24089  indistgp  24090  ehl1eudis  25412  ehl2eudis  25414  elovolmlem  25466  itg2seq  25734  coeeulem  26214  coeeq  26217  aannenlem1  26319  dvntaylp  26361  taylthlem1  26363  taylthlem2  26364  pserdvlem2  26418  lgamgulmlem6  27022  sqff1o  27170  isismt  28627  elee  28987  islno  30849  nmooval  30859  ajfval  30905  h2hcau  31075  h2hlm  31076  hcau  31280  hlimadd  31289  hhcms  31299  hlim0  31331  hhsscms  31374  pjmf1  31812  hosmval  31831  hommval  31832  hodmval  31833  hfsmval  31834  hfmmval  31835  elcnop  31953  ellnop  31954  elhmop  31969  hmopex  31971  nlfnval  31977  elcnfn  31978  ellnfn  31979  dmadjss  31983  dmadjop  31984  adjeu  31985  adjval  31986  hhcno  32000  hhcnf  32001  adjbdln  32179  isst  32309  ishst  32310  maprnin  32830  fpwrelmap  32832  fpwrelmapffs  32833  ismnt  33069  mgcval  33073  fply1  33648  psrmon  33740  zarcmplem  34072  eulerpartleme  34554  eulerpartlemt  34562  eulerpartlemr  34565  eulerpartlemmf  34566  eulerpartlemgvv  34567  eulerpartlemgs2  34571  eulerpartlemn  34572  reprinfz1  34813  breprexplemb  34822  breprexpnat  34825  vtsval  34828  circlemethnat  34832  circlemethhgt  34834  ex-sategoelel12  35662  mrsubff  35747  mrsubrn  35748  msubff  35765  poimirlem3  37997  poimirlem4  37998  poimirlem17  38011  poimirlem20  38014  poimirlem24  38018  poimirlem25  38019  poimirlem29  38023  poimirlem30  38024  poimirlem31  38025  poimirlem32  38026  isrngohom  38339  islfl  39559  islpolN  41982  constmap  43169  mzpclall  43183  mzpf  43192  mzpindd  43202  mzpcompact2lem  43207  eldiophb  43213  mendring  43640  clsk1independent  44497  k0004lem3  44600  mnringmulrcld  44679  dvnprodlem3  46398  fourierdlem70  46626  fourierdlem102  46658  fourierdlem114  46670  etransclem35  46719  hoicvrrex  47006  ovnhoilem1  47051  ovnovollem2  47107  nnsum3primes4  48286  nnsum3primesprm  48288  grimfn  48377  isgrim  48380  rrx2xpref1o  49216  rrx2linesl  49241  line2  49250  line2x  49252  line2y  49253  funcf2lem  49578  aacllem  50298