Theorem elmap 8844

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  Vcvv 3447  ⟶wf 6507  (class class class)co 7387   ↑_m cmap 8799

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 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

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 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392  df-map 8801

This theorem is referenced by:  mapval2  8845  fvmptmap  8854  mapsnconst  8865  mapsncnv  8866  xpmapenlem  9108  pwfseqlem3  10613  tskcard  10734  ingru  10768  rpnnen1lem1  12937  rpnnen1lem3  12938  rpnnen1lem4  12939  rpnnen1lem5  12940  facmapnn  14250  prmreclem2  16888  1arith  16898  vdwlem6  16957  vdwlem7  16958  vdwlem8  16959  vdwlem9  16960  vdwlem11  16962  vdwlem13  16964  prmgapprmo  17033  isfunc  17826  isfuncd  17827  idfucl  17843  cofucl  17850  funcres2b  17859  wunfunc  17863  catcfuccl  18080  funcestrcsetclem9  18109  ismgmhm  18623  ismhm  18712  efmnd1bas  18820  smndex1ibas  18827  smndex1gbas  18829  dfrhm2  20383  isabv  20720  pjdm  21616  pjfval2  21618  psrelbas  21843  psraddcl  21847  psraddclOLD  21848  psrmulcllem  21854  psrvscacl  21860  psr0cl  21861  psrnegcl  21863  psr1cl  21870  subrgpsr  21887  mvrf  21894  mplmon  21942  mplcoe1  21944  coe1fval3  22093  00ply1bas  22124  ply1plusgfvi  22126  coe1z  22149  coe1mul2  22155  coe1tm  22159  pnrmopn  23230  distgp  23986  indistgp  23987  ehl1eudis  25320  ehl2eudis  25322  elovolmlem  25375  itg2seq  25643  coeeulem  26129  coeeq  26132  aannenlem1  26236  dvntaylp  26279  taylthlem1  26281  taylthlem2  26282  taylthlem2OLD  26283  pserdvlem2  26338  lgamgulmlem6  26944  sqff1o  27092  isismt  28461  elee  28821  islno  30682  nmooval  30692  ajfval  30738  h2hcau  30908  h2hlm  30909  hcau  31113  hlimadd  31122  hhcms  31132  hlim0  31164  hhsscms  31207  pjmf1  31645  hosmval  31664  hommval  31665  hodmval  31666  hfsmval  31667  hfmmval  31668  elcnop  31786  ellnop  31787  elhmop  31802  hmopex  31804  nlfnval  31810  elcnfn  31811  ellnfn  31812  dmadjss  31816  dmadjop  31817  adjeu  31818  adjval  31819  hhcno  31833  hhcnf  31834  adjbdln  32012  isst  32142  ishst  32143  maprnin  32654  fpwrelmap  32656  fpwrelmapffs  32657  ismnt  32909  mgcval  32913  fply1  33527  zarcmplem  33871  eulerpartleme  34354  eulerpartlemt  34362  eulerpartlemr  34365  eulerpartlemmf  34366  eulerpartlemgvv  34367  eulerpartlemgs2  34371  eulerpartlemn  34372  reprinfz1  34613  breprexplemb  34622  breprexpnat  34625  vtsval  34628  circlemethnat  34632  circlemethhgt  34634  ex-sategoelel12  35414  mrsubff  35499  mrsubrn  35500  msubff  35517  poimirlem3  37617  poimirlem4  37618  poimirlem17  37631  poimirlem20  37634  poimirlem24  37638  poimirlem25  37639  poimirlem29  37643  poimirlem30  37644  poimirlem31  37645  poimirlem32  37646  isrngohom  37959  islfl  39053  islpolN  41477  constmap  42701  mzpclall  42715  mzpf  42724  mzpindd  42734  mzpcompact2lem  42739  eldiophb  42745  mendring  43177  clsk1independent  44035  k0004lem3  44138  mnringmulrcld  44217  dvnprodlem3  45946  fourierdlem70  46174  fourierdlem102  46206  fourierdlem114  46218  etransclem35  46267  hoicvrrex  46554  ovnhoilem1  46599  ovnovollem2  46655  nnsum3primes4  47789  nnsum3primesprm  47791  grimfn  47879  isgrim  47882  rrx2xpref1o  48707  rrx2linesl  48732  line2  48741  line2x  48743  line2y  48744  funcf2lem  49070  aacllem  49790