Theorem elmap 8857

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

Syntax hints:   ↔ wb 209   ∈ wcel 2145  Vcvv 3457  ⟶wf 6521  (class class class)co 7400   ↑_m cmap 8812

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-pow 5327  ax-pr 5395  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-fv 6533  df-ov 7403  df-oprab 7404  df-mpo 7405  df-map 8814

This theorem is referenced by:  mapval2  8858  fvmptmap  8867  mapsnconst  8878  mapsncnv  8879  xpmapenlem  9120  pwfseqlem3  10633  tskcard  10754  ingru  10788  rpnnen1lem1  12993  rpnnen1lem3  12994  rpnnen1lem4  12995  rpnnen1lem5  12996  facmapnn  14312  prmreclem2  16967  1arith  16977  vdwlem6  17036  vdwlem7  17037  vdwlem8  17038  vdwlem9  17039  vdwlem11  17041  vdwlem13  17043  prmgapprmo  17112  isfunc  17911  isfuncd  17912  idfucl  17928  cofucl  17935  funcres2b  17944  wunfunc  17948  catcfuccl  18165  funcestrcsetclem9  18194  ismgmhm  18744  ismhm  18833  efmnd1bas  18942  smndex1ibas  18949  smndex1gbas  18951  smndex1gbasOLD  18952  dfrhm2  20547  isabv  20883  pjdm  21817  pjfval2  21819  psrelbas  22045  psraddcl  22049  psrmulcllem  22055  psrvscacl  22061  psr0cl  22062  psrnegcl  22064  psr1cl  22070  subrgpsr  22087  mvrf  22094  mplmon  22146  mplcoe1  22148  coe1fval3  22328  00ply1bas  22359  ply1plusgfvi  22361  coe1z  22384  coe1mul2  22390  coe1tm  22394  pnrmopn  23461  distgp  24217  indistgp  24218  ehl1eudis  25540  ehl2eudis  25542  elovolmlem  25594  itg2seq  25862  coeeulem  26342  coeeq  26345  aannenlem1  26450  dvntaylp  26492  taylthlem1  26494  taylthlem2  26495  pserdvlem2  26549  lgamgulmlem6  27156  sqff1o  27304  isismt  28761  elee  29152  islno  31014  nmooval  31024  ajfval  31070  h2hcau  31240  h2hlm  31241  hcau  31445  hlimadd  31454  hhcms  31464  hlim0  31496  hhsscms  31539  pjmf1  31977  hosmval  31996  hommval  31997  hodmval  31998  hfsmval  31999  hfmmval  32000  elcnop  32118  ellnop  32119  elhmop  32134  hmopex  32136  nlfnval  32142  elcnfn  32143  ellnfn  32144  dmadjss  32148  dmadjop  32149  adjeu  32150  adjval  32151  hhcno  32165  hhcnf  32166  adjbdln  32344  isst  32474  ishst  32475  maprnin  32988  fpwrelmap  32990  fpwrelmapffs  32991  ismnt  33216  mgcval  33220  fply1  33765  psrmon  33856  zarcmplem  34188  eulerpartleme  34670  eulerpartlemt  34678  eulerpartlemr  34681  eulerpartlemmf  34682  eulerpartlemgvv  34683  eulerpartlemgs2  34687  eulerpartlemn  34688  reprinfz1  34926  breprexplemb  34935  breprexpnat  34938  vtsval  34941  circlemethnat  34945  circlemethhgt  34947  ex-sategoelel12  35790  mrsubff  35875  mrsubrn  35876  msubff  35893  poimirlem3  38134  poimirlem4  38135  poimirlem17  38148  poimirlem20  38151  poimirlem24  38155  poimirlem25  38156  poimirlem29  38160  poimirlem30  38161  poimirlem31  38162  poimirlem32  38163  isrngohom  38476  islfl  39696  islpolN  42119  constmap  43306  mzpclall  43320  mzpf  43329  mzpindd  43339  mzpcompact2lem  43344  eldiophb  43350  mendring  43777  clsk1independent  44634  k0004lem3  44737  mnringmulrcld  44816  dvnprodlem3  46520  fourierdlem70  46748  fourierdlem102  46780  fourierdlem114  46792  etransclem35  46841  hoicvrrex  47128  ovnhoilem1  47173  ovnovollem2  47229  nnsum3primes4  48408  nnsum3primesprm  48410  grimfn  48499  isgrim  48502  rrx2xpref1o  49349  rrx2linesl  49374  line2  49383  line2x  49385  line2y  49386  funcf2lem  49710  aacllem  50430