Theorem elmap 8276

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	⊢ (𝐹 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐹:𝐵⟶𝐴)

Proof of Theorem elmap

Step	Hyp	Ref	Expression
1		elmap.1	. 2 ⊢ 𝐴 ∈ V
2		elmap.2	. 2 ⊢ 𝐵 ∈ V
3		elmapg 8260	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐹 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐹:𝐵⟶𝐴))
4	1, 2, 3	mp2an 688	1 ⊢ (𝐹 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐹:𝐵⟶𝐴)

Syntax hints:   ↔ wb 207   ∈ wcel 2079  Vcvv 3432  ⟶wf 6213  (class class class)co 7007   ↑_𝑚 cmap 8247

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767  ax-sep 5088  ax-nul 5095  ax-pow 5150  ax-pr 5214  ax-un 7310

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-mo 2574  df-eu 2610  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3434  df-sbc 3702  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-nul 4207  df-if 4376  df-pw 4449  df-sn 4467  df-pr 4469  df-op 4473  df-uni 4740  df-br 4957  df-opab 5019  df-id 5340  df-xp 5441  df-rel 5442  df-cnv 5443  df-co 5444  df-dm 5445  df-rn 5446  df-iota 6181  df-fun 6219  df-fn 6220  df-f 6221  df-fv 6225  df-ov 7010  df-oprab 7011  df-mpo 7012  df-map 8249

This theorem is referenced by:  mapval2  8277  fvmptmap  8285  mapsnconst  8295  mapsncnv  8296  xpmapenlem  8521  pwfseqlem3  9917  tskcard  10038  ingru  10072  rpnnen1lem1  12216  rpnnen1lem3  12217  rpnnen1lem4  12218  rpnnen1lem5  12219  facmapnn  13483  prmreclem2  16070  1arith  16080  vdwlem6  16139  vdwlem7  16140  vdwlem8  16141  vdwlem9  16142  vdwlem11  16144  vdwlem13  16146  prmgapprmo  16215  isfunc  16951  isfuncd  16952  idfucl  16968  cofucl  16975  funcres2b  16984  wunfunc  16986  catcfuccl  17186  funcestrcsetclem9  17215  ismhm  17764  symgval  18226  dfrhm2  19147  isabv  19268  psrelbas  19835  psraddcl  19839  psrmulcllem  19843  psrvscacl  19849  psr0cl  19850  psrnegcl  19852  psr1cl  19858  subrgpsr  19875  mvrf  19880  mplmon  19919  mplcoe1  19921  coe1fval3  20047  00ply1bas  20079  ply1plusgfvi  20081  coe1z  20102  coe1mul2  20108  coe1tm  20112  pjdm  20521  pjfval2  20523  pnrmopn  21623  distgp  22379  indistgp  22380  ehl1eudis  23694  ehl2eudis  23696  elovolmlem  23746  itg2seq  24014  coeeulem  24485  coeeq  24488  aannenlem1  24588  dvntaylp  24630  taylthlem1  24632  taylthlem2  24633  pserdvlem2  24687  lgamgulmlem6  25281  sqff1o  25429  isismt  25990  elee  26351  islno  28209  nmooval  28219  ajfval  28265  h2hcau  28435  h2hlm  28436  hcau  28640  hlimadd  28649  hhcms  28659  hlim0  28691  hhsscms  28734  pjmf1  29172  hosmval  29191  hommval  29192  hodmval  29193  hfsmval  29194  hfmmval  29195  elcnop  29313  ellnop  29314  elhmop  29329  hmopex  29331  nlfnval  29337  elcnfn  29338  ellnfn  29339  dmadjss  29343  dmadjop  29344  adjeu  29345  adjval  29346  hhcno  29360  hhcnf  29361  adjbdln  29539  isst  29669  ishst  29670  maprnin  30128  fpwrelmap  30130  fpwrelmapffs  30131  fply1  30534  eulerpartleme  31194  eulerpartlemt  31202  eulerpartlemr  31205  eulerpartlemmf  31206  eulerpartlemgvv  31207  eulerpartlemgs2  31211  eulerpartlemn  31212  reprinfz1  31466  breprexplemb  31475  breprexpnat  31478  vtsval  31481  circlemethnat  31485  circlemethhgt  31487  mrsubff  32312  mrsubrn  32313  msubff  32330  poimirlem3  34372  poimirlem4  34373  poimirlem17  34386  poimirlem20  34389  poimirlem24  34393  poimirlem25  34394  poimirlem29  34398  poimirlem30  34399  poimirlem31  34400  poimirlem32  34401  isrngohom  34721  islfl  35677  islpolN  38100  constmap  38745  mzpclall  38759  mzpf  38768  mzpindd  38778  mzpcompact2lem  38783  eldiophb  38789  mendring  39228  clsk1independent  39832  k0004lem3  39935  dvnprodlem3  41728  fourierdlem70  41957  fourierdlem102  41989  fourierdlem114  42001  etransclem35  42050  hoicvrrex  42334  ovnhoilem1  42379  ovnovollem2  42435  nnsum3primes4  43389  nnsum3primesprm  43391  ismgmhm  43486  rrx2xpref1o  44140  rrx2linesl  44165  line2  44174  line2x  44176  line2y  44177  aacllem  44336