Theorem elmap 8617

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

Syntax hints:   ↔ wb 205   ∈ wcel 2108  Vcvv 3422  ⟶wf 6414  (class class class)co 7255   ↑_m cmap 8573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-map 8575

This theorem is referenced by:  mapval2  8618  fvmptmap  8627  mapsnconst  8638  mapsncnv  8639  xpmapenlem  8880  pwfseqlem3  10347  tskcard  10468  ingru  10502  rpnnen1lem1  12647  rpnnen1lem3  12648  rpnnen1lem4  12649  rpnnen1lem5  12650  facmapnn  13927  prmreclem2  16546  1arith  16556  vdwlem6  16615  vdwlem7  16616  vdwlem8  16617  vdwlem9  16618  vdwlem11  16620  vdwlem13  16622  prmgapprmo  16691  isfunc  17495  isfuncd  17496  idfucl  17512  cofucl  17519  funcres2b  17528  wunfunc  17530  wunfuncOLD  17531  catcfuccl  17750  catcfucclOLD  17751  funcestrcsetclem9  17781  ismhm  18347  efmnd1bas  18447  smndex1ibas  18454  smndex1gbas  18456  dfrhm2  19876  isabv  19994  pjdm  20824  pjfval2  20826  psrelbas  21058  psraddcl  21062  psrmulcllem  21066  psrvscacl  21072  psr0cl  21073  psrnegcl  21075  psr1cl  21081  subrgpsr  21098  mvrf  21103  mplmon  21146  mplcoe1  21148  coe1fval3  21289  00ply1bas  21321  ply1plusgfvi  21323  coe1z  21344  coe1mul2  21350  coe1tm  21354  pnrmopn  22402  distgp  23158  indistgp  23159  ehl1eudis  24489  ehl2eudis  24491  elovolmlem  24543  itg2seq  24812  coeeulem  25290  coeeq  25293  aannenlem1  25393  dvntaylp  25435  taylthlem1  25437  taylthlem2  25438  pserdvlem2  25492  lgamgulmlem6  26088  sqff1o  26236  isismt  26799  elee  27165  islno  29016  nmooval  29026  ajfval  29072  h2hcau  29242  h2hlm  29243  hcau  29447  hlimadd  29456  hhcms  29466  hlim0  29498  hhsscms  29541  pjmf1  29979  hosmval  29998  hommval  29999  hodmval  30000  hfsmval  30001  hfmmval  30002  elcnop  30120  ellnop  30121  elhmop  30136  hmopex  30138  nlfnval  30144  elcnfn  30145  ellnfn  30146  dmadjss  30150  dmadjop  30151  adjeu  30152  adjval  30153  hhcno  30167  hhcnf  30168  adjbdln  30346  isst  30476  ishst  30477  maprnin  30968  fpwrelmap  30970  fpwrelmapffs  30971  ismnt  31163  mgcval  31167  fply1  31569  zarcmplem  31733  eulerpartleme  32230  eulerpartlemt  32238  eulerpartlemr  32241  eulerpartlemmf  32242  eulerpartlemgvv  32243  eulerpartlemgs2  32247  eulerpartlemn  32248  reprinfz1  32502  breprexplemb  32511  breprexpnat  32514  vtsval  32517  circlemethnat  32521  circlemethhgt  32523  ex-sategoelel12  33289  mrsubff  33374  mrsubrn  33375  msubff  33392  poimirlem3  35707  poimirlem4  35708  poimirlem17  35721  poimirlem20  35724  poimirlem24  35728  poimirlem25  35729  poimirlem29  35733  poimirlem30  35734  poimirlem31  35735  poimirlem32  35736  isrngohom  36050  islfl  37001  islpolN  39424  constmap  40451  mzpclall  40465  mzpf  40474  mzpindd  40484  mzpcompact2lem  40489  eldiophb  40495  mendring  40933  clsk1independent  41545  k0004lem3  41648  mnringmulrcld  41735  dvnprodlem3  43379  fourierdlem70  43607  fourierdlem102  43639  fourierdlem114  43651  etransclem35  43700  hoicvrrex  43984  ovnhoilem1  44029  ovnovollem2  44085  nnsum3primes4  45128  nnsum3primesprm  45130  ismgmhm  45225  rrx2xpref1o  45952  rrx2linesl  45977  line2  45986  line2x  45988  line2y  45989  funcf2lem  46187  aacllem  46391