Theorem elmap 8927

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2147  Vcvv 3454  ⟶wf 6554  (class class class)co 7443   ↑_m cmap 8875

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-pow 5331  ax-pr 5395  ax-un 7775

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-fv 6566  df-ov 7446  df-oprab 7447  df-mpo 7448  df-map 8877

This theorem is used by:  mapval2  8928  fvmptmap  8937  mapsnconst  8948  mapsncnv  8949  xpmapenlem  9191  pwfseqlem3  10772  tskcard  10893  ingru  10927  rpnnen1lem1  13133  rpnnen1lem3  13134  rpnnen1lem4  13135  rpnnen1lem5  13136  facmapnn  14456  prmreclem2  17124  1arith  17134  vdwlem6  17193  vdwlem7  17194  vdwlem8  17195  vdwlem9  17196  vdwlem11  17198  vdwlem13  17200  prmgapprmo  17269  isfunc  18068  isfuncd  18069  idfucl  18085  cofucl  18092  funcres2b  18101  wunfunc  18105  catcfuccl  18322  funcestrcsetclem9  18351  ismgmhm  18914  ismhm  19009  efmnd1bas  19118  smndex1ibas  19125  smndex1gbas  19127  smndex1gbasOLD  19128  dfrhm2  20734  isrhm0  20736  isabv  21098  pjdm  22043  pjfval2  22045  psrelbas  22273  psraddcl  22277  psrmulcllem  22283  psrvscacl  22289  psr0cl  22290  psrnegcl  22292  psr1cl  22298  subrgpsr  22315  mvrf  22322  mplmon  22374  mplcoe1  22376  coe1fval3  22556  00ply1bas  22587  ply1plusgfvi  22589  coe1z  22612  coe1mul2  22618  coe1tm  22622  pnrmopn  23691  distgp  24448  indistgp  24449  ehl1eudis  25771  ehl2eudis  25773  elovolmlem  25825  itg2seq  26093  coeeulem  26573  coeeq  26576  aannenlem1  26685  dvntaylp  26728  taylthlem1  26730  taylthlem2  26731  pserdvlem2  26785  lgamgulmlem6  27391  sqff1o  27539  isismt  29027  elee  29501  islno  31385  nmooval  31395  ajfval  31441  h2hcau  31611  h2hlm  31612  hcau  31816  hlimadd  31825  hhcms  31835  hlim0  31867  hhsscms  31910  pjmf1  32348  hosmval  32367  hommval  32368  hodmval  32369  hfsmval  32370  hfmmval  32371  elcnop  32489  ellnop  32490  elhmop  32505  hmopex  32507  nlfnval  32513  elcnfn  32514  ellnfn  32515  dmadjss  32519  dmadjop  32520  adjeu  32521  adjval  32522  hhcno  32536  hhcnf  32537  adjbdln  32715  isst  32845  ishst  32846  maprnin  33393  fpwrelmap  33395  fpwrelmapffs  33396  ismnt  33614  mgcval  33618  fply1  34160  psrmon  34251  zarcmplem  34583  eulerpartleme  35065  eulerpartlemt  35073  eulerpartlemr  35076  eulerpartlemmf  35077  eulerpartlemgvv  35078  eulerpartlemgs2  35082  eulerpartlemn  35083  reprinfz1  35321  breprexplemb  35330  breprexpnat  35333  vtsval  35336  circlemethnat  35340  circlemethhgt  35342  ex-sategoelel12  36359  mrsubff  36444  mrsubrn  36445  msubff  36462  poimirlem3  38733  poimirlem4  38734  poimirlem17  38747  poimirlem20  38750  poimirlem24  38754  poimirlem25  38755  poimirlem29  38759  poimirlem30  38760  poimirlem31  38761  poimirlem32  38762  isrngohom  39091  islfl  40309  islpolN  42732  constmap  43917  mzpclall  43931  mzpf  43940  mzpindd  43950  mzpcompact2lem  43955  eldiophb  43961  mendring  44382  clsk1independent  45238  k0004lem3  45341  mnringmulrcld  45418  dvnprodlem3  47163  fourierdlem70  47391  fourierdlem102  47423  fourierdlem114  47435  etransclem35  47484  hoicvrrex  47771  ovnhoilem1  47816  ovnovollem2  47872  nnsum3primes4  49091  nnsum3primesprm  49093  grimfn  49182  isgrim  49185  line2  50069  line2x  50071  line2y  50072  funcf2lem  50400  aacllem  51219  crosspcld  51239  veronesematbasd  51260  veroquadmodzerod  51264  veroquadnolindfd  51265  veroquaddetzerod  51266