Theorem elmap 8882

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2145  Vcvv 3453  ⟶wf 6533  (class class class)co 7417   ↑_m cmap 8830

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-pow 5334  ax-pr 5402  ax-un 7740

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 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-ov 7420  df-oprab 7421  df-mpo 7422  df-map 8832

This theorem is used by:  mapval2  8883  fvmptmap  8892  mapsnconst  8903  mapsncnv  8904  xpmapenlem  9146  pwfseqlem3  10673  tskcard  10794  ingru  10828  rpnnen1lem1  13032  rpnnen1lem3  13033  rpnnen1lem4  13034  rpnnen1lem5  13035  facmapnn  14353  prmreclem2  17015  1arith  17025  vdwlem6  17084  vdwlem7  17085  vdwlem8  17086  vdwlem9  17087  vdwlem11  17089  vdwlem13  17091  prmgapprmo  17160  isfunc  17959  isfuncd  17960  idfucl  17976  cofucl  17983  funcres2b  17992  wunfunc  17996  catcfuccl  18213  funcestrcsetclem9  18242  ismgmhm  18804  ismhm  18899  efmnd1bas  19008  smndex1ibas  19015  smndex1gbas  19017  smndex1gbasOLD  19018  dfrhm2  20621  isrhm0  20623  isabv  20983  pjdm  21926  pjfval2  21928  psrelbas  22156  psraddcl  22160  psrmulcllem  22166  psrvscacl  22172  psr0cl  22173  psrnegcl  22175  psr1cl  22181  subrgpsr  22198  mvrf  22205  mplmon  22257  mplcoe1  22259  coe1fval3  22439  00ply1bas  22470  ply1plusgfvi  22472  coe1z  22495  coe1mul2  22501  coe1tm  22505  pnrmopn  23574  distgp  24331  indistgp  24332  ehl1eudis  25654  ehl2eudis  25656  elovolmlem  25708  itg2seq  25976  coeeulem  26457  coeeq  26460  aannenlem1  26571  dvntaylp  26614  taylthlem1  26616  taylthlem2  26617  pserdvlem2  26671  lgamgulmlem6  27278  sqff1o  27426  isismt  28884  elee  29358  islno  31242  nmooval  31252  ajfval  31298  h2hcau  31468  h2hlm  31469  hcau  31673  hlimadd  31682  hhcms  31692  hlim0  31724  hhsscms  31767  pjmf1  32205  hosmval  32224  hommval  32225  hodmval  32226  hfsmval  32227  hfmmval  32228  elcnop  32346  ellnop  32347  elhmop  32362  hmopex  32364  nlfnval  32370  elcnfn  32371  ellnfn  32372  dmadjss  32376  dmadjop  32377  adjeu  32378  adjval  32379  hhcno  32393  hhcnf  32394  adjbdln  32572  isst  32702  ishst  32703  maprnin  33210  fpwrelmap  33212  fpwrelmapffs  33213  ismnt  33431  mgcval  33435  fply1  33976  psrmon  34067  zarcmplem  34399  eulerpartleme  34882  eulerpartlemt  34890  eulerpartlemr  34893  eulerpartlemmf  34894  eulerpartlemgvv  34895  eulerpartlemgs2  34899  eulerpartlemn  34900  reprinfz1  35138  breprexplemb  35147  breprexpnat  35150  vtsval  35153  circlemethnat  35157  circlemethhgt  35159  ex-sategoelel12  36014  mrsubff  36099  mrsubrn  36100  msubff  36117  poimirlem3  38380  poimirlem4  38381  poimirlem17  38394  poimirlem20  38397  poimirlem24  38401  poimirlem25  38402  poimirlem29  38406  poimirlem30  38407  poimirlem31  38408  poimirlem32  38409  isrngohom  38723  islfl  39941  islpolN  42364  constmap  43566  mzpclall  43580  mzpf  43589  mzpindd  43599  mzpcompact2lem  43604  eldiophb  43610  mendring  44037  clsk1independent  44894  k0004lem3  44997  mnringmulrcld  45074  dvnprodlem3  46784  fourierdlem70  47012  fourierdlem102  47044  fourierdlem114  47056  etransclem35  47105  hoicvrrex  47392  ovnhoilem1  47437  ovnovollem2  47493  nnsum3primes4  48712  nnsum3primesprm  48714  grimfn  48803  isgrim  48806  rrx2xpref1o  49656  rrx2linesl  49681  line2  49690  line2x  49692  line2y  49693  funcf2lem  50015  aacllem  50780  crosspcld  50800  veronesematbasd  50821  veroquadmodzerod  50825  veroquadnolindfd  50826  veroquaddetzerod  50827