Theorem elmap 8805

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  Vcvv 3438  ⟶wf 6482  (class class class)co 7353   ↑_m cmap 8760

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-fv 6494  df-ov 7356  df-oprab 7357  df-mpo 7358  df-map 8762

This theorem is referenced by:  mapval2  8806  fvmptmap  8815  mapsnconst  8826  mapsncnv  8827  xpmapenlem  9068  pwfseqlem3  10573  tskcard  10694  ingru  10728  rpnnen1lem1  12897  rpnnen1lem3  12898  rpnnen1lem4  12899  rpnnen1lem5  12900  facmapnn  14210  prmreclem2  16847  1arith  16857  vdwlem6  16916  vdwlem7  16917  vdwlem8  16918  vdwlem9  16919  vdwlem11  16921  vdwlem13  16923  prmgapprmo  16992  isfunc  17789  isfuncd  17790  idfucl  17806  cofucl  17813  funcres2b  17822  wunfunc  17826  catcfuccl  18043  funcestrcsetclem9  18072  ismgmhm  18588  ismhm  18677  efmnd1bas  18785  smndex1ibas  18792  smndex1gbas  18794  dfrhm2  20377  isabv  20714  pjdm  21632  pjfval2  21634  psrelbas  21859  psraddcl  21863  psraddclOLD  21864  psrmulcllem  21870  psrvscacl  21876  psr0cl  21877  psrnegcl  21879  psr1cl  21886  subrgpsr  21903  mvrf  21910  mplmon  21958  mplcoe1  21960  coe1fval3  22109  00ply1bas  22140  ply1plusgfvi  22142  coe1z  22165  coe1mul2  22171  coe1tm  22175  pnrmopn  23246  distgp  24002  indistgp  24003  ehl1eudis  25336  ehl2eudis  25338  elovolmlem  25391  itg2seq  25659  coeeulem  26145  coeeq  26148  aannenlem1  26252  dvntaylp  26295  taylthlem1  26297  taylthlem2  26298  taylthlem2OLD  26299  pserdvlem2  26354  lgamgulmlem6  26960  sqff1o  27108  isismt  28497  elee  28857  islno  30715  nmooval  30725  ajfval  30771  h2hcau  30941  h2hlm  30942  hcau  31146  hlimadd  31155  hhcms  31165  hlim0  31197  hhsscms  31240  pjmf1  31678  hosmval  31697  hommval  31698  hodmval  31699  hfsmval  31700  hfmmval  31701  elcnop  31819  ellnop  31820  elhmop  31835  hmopex  31837  nlfnval  31843  elcnfn  31844  ellnfn  31845  dmadjss  31849  dmadjop  31850  adjeu  31851  adjval  31852  hhcno  31866  hhcnf  31867  adjbdln  32045  isst  32175  ishst  32176  maprnin  32687  fpwrelmap  32689  fpwrelmapffs  32690  ismnt  32938  mgcval  32942  fply1  33503  zarcmplem  33847  eulerpartleme  34330  eulerpartlemt  34338  eulerpartlemr  34341  eulerpartlemmf  34342  eulerpartlemgvv  34343  eulerpartlemgs2  34347  eulerpartlemn  34348  reprinfz1  34589  breprexplemb  34598  breprexpnat  34601  vtsval  34604  circlemethnat  34608  circlemethhgt  34610  ex-sategoelel12  35399  mrsubff  35484  mrsubrn  35485  msubff  35502  poimirlem3  37602  poimirlem4  37603  poimirlem17  37616  poimirlem20  37619  poimirlem24  37623  poimirlem25  37624  poimirlem29  37628  poimirlem30  37629  poimirlem31  37630  poimirlem32  37631  isrngohom  37944  islfl  39038  islpolN  41462  constmap  42686  mzpclall  42700  mzpf  42709  mzpindd  42719  mzpcompact2lem  42724  eldiophb  42730  mendring  43161  clsk1independent  44019  k0004lem3  44122  mnringmulrcld  44201  dvnprodlem3  45930  fourierdlem70  46158  fourierdlem102  46190  fourierdlem114  46202  etransclem35  46251  hoicvrrex  46538  ovnhoilem1  46583  ovnovollem2  46639  nnsum3primes4  47773  nnsum3primesprm  47775  grimfn  47864  isgrim  47867  rrx2xpref1o  48704  rrx2linesl  48729  line2  48738  line2x  48740  line2y  48741  funcf2lem  49067  aacllem  49787