Theorem elmap 8847

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  Vcvv 3450  ⟶wf 6510  (class class class)co 7390   ↑_m cmap 8802

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 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-map 8804

This theorem is referenced by:  mapval2  8848  fvmptmap  8857  mapsnconst  8868  mapsncnv  8869  xpmapenlem  9114  pwfseqlem3  10620  tskcard  10741  ingru  10775  rpnnen1lem1  12944  rpnnen1lem3  12945  rpnnen1lem4  12946  rpnnen1lem5  12947  facmapnn  14257  prmreclem2  16895  1arith  16905  vdwlem6  16964  vdwlem7  16965  vdwlem8  16966  vdwlem9  16967  vdwlem11  16969  vdwlem13  16971  prmgapprmo  17040  isfunc  17833  isfuncd  17834  idfucl  17850  cofucl  17857  funcres2b  17866  wunfunc  17870  catcfuccl  18087  funcestrcsetclem9  18116  ismgmhm  18630  ismhm  18719  efmnd1bas  18827  smndex1ibas  18834  smndex1gbas  18836  dfrhm2  20390  isabv  20727  pjdm  21623  pjfval2  21625  psrelbas  21850  psraddcl  21854  psraddclOLD  21855  psrmulcllem  21861  psrvscacl  21867  psr0cl  21868  psrnegcl  21870  psr1cl  21877  subrgpsr  21894  mvrf  21901  mplmon  21949  mplcoe1  21951  coe1fval3  22100  00ply1bas  22131  ply1plusgfvi  22133  coe1z  22156  coe1mul2  22162  coe1tm  22166  pnrmopn  23237  distgp  23993  indistgp  23994  ehl1eudis  25327  ehl2eudis  25329  elovolmlem  25382  itg2seq  25650  coeeulem  26136  coeeq  26139  aannenlem1  26243  dvntaylp  26286  taylthlem1  26288  taylthlem2  26289  taylthlem2OLD  26290  pserdvlem2  26345  lgamgulmlem6  26951  sqff1o  27099  isismt  28468  elee  28828  islno  30689  nmooval  30699  ajfval  30745  h2hcau  30915  h2hlm  30916  hcau  31120  hlimadd  31129  hhcms  31139  hlim0  31171  hhsscms  31214  pjmf1  31652  hosmval  31671  hommval  31672  hodmval  31673  hfsmval  31674  hfmmval  31675  elcnop  31793  ellnop  31794  elhmop  31809  hmopex  31811  nlfnval  31817  elcnfn  31818  ellnfn  31819  dmadjss  31823  dmadjop  31824  adjeu  31825  adjval  31826  hhcno  31840  hhcnf  31841  adjbdln  32019  isst  32149  ishst  32150  maprnin  32661  fpwrelmap  32663  fpwrelmapffs  32664  ismnt  32916  mgcval  32920  fply1  33534  zarcmplem  33878  eulerpartleme  34361  eulerpartlemt  34369  eulerpartlemr  34372  eulerpartlemmf  34373  eulerpartlemgvv  34374  eulerpartlemgs2  34378  eulerpartlemn  34379  reprinfz1  34620  breprexplemb  34629  breprexpnat  34632  vtsval  34635  circlemethnat  34639  circlemethhgt  34641  ex-sategoelel12  35421  mrsubff  35506  mrsubrn  35507  msubff  35524  poimirlem3  37624  poimirlem4  37625  poimirlem17  37638  poimirlem20  37641  poimirlem24  37645  poimirlem25  37646  poimirlem29  37650  poimirlem30  37651  poimirlem31  37652  poimirlem32  37653  isrngohom  37966  islfl  39060  islpolN  41484  constmap  42708  mzpclall  42722  mzpf  42731  mzpindd  42741  mzpcompact2lem  42746  eldiophb  42752  mendring  43184  clsk1independent  44042  k0004lem3  44145  mnringmulrcld  44224  dvnprodlem3  45953  fourierdlem70  46181  fourierdlem102  46213  fourierdlem114  46225  etransclem35  46274  hoicvrrex  46561  ovnhoilem1  46606  ovnovollem2  46662  nnsum3primes4  47793  nnsum3primesprm  47795  grimfn  47883  isgrim  47886  rrx2xpref1o  48711  rrx2linesl  48736  line2  48745  line2x  48747  line2y  48748  funcf2lem  49074  aacllem  49794