Theorem elmap 8865

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

Syntax hints:   ↔ wb 205   ∈ wcel 2107  Vcvv 3475  ⟶wf 6540  (class class class)co 7409   ↑_m cmap 8820

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-map 8822

This theorem is referenced by:  mapval2  8866  fvmptmap  8875  mapsnconst  8886  mapsncnv  8887  xpmapenlem  9144  pwfseqlem3  10655  tskcard  10776  ingru  10810  rpnnen1lem1  12962  rpnnen1lem3  12963  rpnnen1lem4  12964  rpnnen1lem5  12965  facmapnn  14245  prmreclem2  16850  1arith  16860  vdwlem6  16919  vdwlem7  16920  vdwlem8  16921  vdwlem9  16922  vdwlem11  16924  vdwlem13  16926  prmgapprmo  16995  isfunc  17814  isfuncd  17815  idfucl  17831  cofucl  17838  funcres2b  17847  wunfunc  17849  wunfuncOLD  17850  catcfuccl  18069  catcfucclOLD  18070  funcestrcsetclem9  18100  ismhm  18673  efmnd1bas  18774  smndex1ibas  18781  smndex1gbas  18783  dfrhm2  20253  isabv  20427  pjdm  21262  pjfval2  21264  psrelbas  21498  psraddcl  21502  psrmulcllem  21506  psrvscacl  21512  psr0cl  21513  psrnegcl  21515  psr1cl  21522  subrgpsr  21539  mvrf  21544  mplmon  21590  mplcoe1  21592  coe1fval3  21732  00ply1bas  21762  ply1plusgfvi  21764  coe1z  21785  coe1mul2  21791  coe1tm  21795  pnrmopn  22847  distgp  23603  indistgp  23604  ehl1eudis  24937  ehl2eudis  24939  elovolmlem  24991  itg2seq  25260  coeeulem  25738  coeeq  25741  aannenlem1  25841  dvntaylp  25883  taylthlem1  25885  taylthlem2  25886  pserdvlem2  25940  lgamgulmlem6  26538  sqff1o  26686  isismt  27785  elee  28152  islno  30006  nmooval  30016  ajfval  30062  h2hcau  30232  h2hlm  30233  hcau  30437  hlimadd  30446  hhcms  30456  hlim0  30488  hhsscms  30531  pjmf1  30969  hosmval  30988  hommval  30989  hodmval  30990  hfsmval  30991  hfmmval  30992  elcnop  31110  ellnop  31111  elhmop  31126  hmopex  31128  nlfnval  31134  elcnfn  31135  ellnfn  31136  dmadjss  31140  dmadjop  31141  adjeu  31142  adjval  31143  hhcno  31157  hhcnf  31158  adjbdln  31336  isst  31466  ishst  31467  maprnin  31956  fpwrelmap  31958  fpwrelmapffs  31959  ismnt  32153  mgcval  32157  fply1  32637  zarcmplem  32861  eulerpartleme  33362  eulerpartlemt  33370  eulerpartlemr  33373  eulerpartlemmf  33374  eulerpartlemgvv  33375  eulerpartlemgs2  33379  eulerpartlemn  33380  reprinfz1  33634  breprexplemb  33643  breprexpnat  33646  vtsval  33649  circlemethnat  33653  circlemethhgt  33655  ex-sategoelel12  34418  mrsubff  34503  mrsubrn  34504  msubff  34521  poimirlem3  36491  poimirlem4  36492  poimirlem17  36505  poimirlem20  36508  poimirlem24  36512  poimirlem25  36513  poimirlem29  36517  poimirlem30  36518  poimirlem31  36519  poimirlem32  36520  isrngohom  36833  islfl  37930  islpolN  40354  constmap  41451  mzpclall  41465  mzpf  41474  mzpindd  41484  mzpcompact2lem  41489  eldiophb  41495  mendring  41934  clsk1independent  42797  k0004lem3  42900  mnringmulrcld  42987  dvnprodlem3  44664  fourierdlem70  44892  fourierdlem102  44924  fourierdlem114  44936  etransclem35  44985  hoicvrrex  45272  ovnhoilem1  45317  ovnovollem2  45373  nnsum3primes4  46456  nnsum3primesprm  46458  ismgmhm  46553  rrx2xpref1o  47404  rrx2linesl  47429  line2  47438  line2x  47440  line2y  47441  funcf2lem  47638  aacllem  47848