Theorem elmap 8902

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2144  Vcvv 3450  ⟶wf 6534  (class class class)co 7420   ↑_m cmap 8850

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pow 5326  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425  df-map 8852

This theorem is used by:  mapval2  8903  fvmptmap  8912  mapsnconst  8923  mapsncnv  8924  xpmapenlem  9166  pwfseqlem3  10748  tskcard  10869  ingru  10903  rpnnen1lem1  13109  rpnnen1lem3  13110  rpnnen1lem4  13111  rpnnen1lem5  13112  facmapnn  14432  prmreclem2  17100  1arith  17110  vdwlem6  17169  vdwlem7  17170  vdwlem8  17171  vdwlem9  17172  vdwlem11  17174  vdwlem13  17176  prmgapprmo  17245  isfunc  18044  isfuncd  18045  idfucl  18061  cofucl  18068  funcres2b  18077  wunfunc  18081  catcfuccl  18298  funcestrcsetclem9  18327  ismgmhm  18890  ismhm  18985  efmnd1bas  19094  smndex1ibas  19101  smndex1gbas  19103  smndex1gbasOLD  19104  dfrhm2  20709  isrhm0  20711  isabv  21073  pjdm  22018  pjfval2  22020  psrelbas  22248  psraddcl  22252  psrmulcllem  22258  psrvscacl  22264  psr0cl  22265  psrnegcl  22267  psr1cl  22273  subrgpsr  22290  mvrf  22297  mplmon  22349  mplcoe1  22351  coe1fval3  22531  00ply1bas  22562  ply1plusgfvi  22564  coe1z  22587  coe1mul2  22593  coe1tm  22597  pnrmopn  23666  distgp  24423  indistgp  24424  ehl1eudis  25746  ehl2eudis  25748  elovolmlem  25800  itg2seq  26068  coeeulem  26548  coeeq  26551  aannenlem1  26660  dvntaylp  26703  taylthlem1  26705  taylthlem2  26706  pserdvlem2  26760  lgamgulmlem6  27366  sqff1o  27514  isismt  29002  elee  29476  islno  31360  nmooval  31370  ajfval  31416  h2hcau  31586  h2hlm  31587  hcau  31791  hlimadd  31800  hhcms  31810  hlim0  31842  hhsscms  31885  pjmf1  32323  hosmval  32342  hommval  32343  hodmval  32344  hfsmval  32345  hfmmval  32346  elcnop  32464  ellnop  32465  elhmop  32480  hmopex  32482  nlfnval  32488  elcnfn  32489  ellnfn  32490  dmadjss  32494  dmadjop  32495  adjeu  32496  adjval  32497  hhcno  32511  hhcnf  32512  adjbdln  32690  isst  32820  ishst  32821  maprnin  33369  fpwrelmap  33371  fpwrelmapffs  33372  ismnt  33590  mgcval  33594  fply1  34136  psrmon  34227  zarcmplem  34559  eulerpartleme  35041  eulerpartlemt  35049  eulerpartlemr  35052  eulerpartlemmf  35053  eulerpartlemgvv  35054  eulerpartlemgs2  35058  eulerpartlemn  35059  reprinfz1  35297  breprexplemb  35306  breprexpnat  35309  vtsval  35312  circlemethnat  35316  circlemethhgt  35318  ex-sategoelel12  36278  mrsubff  36363  mrsubrn  36364  msubff  36381  poimirlem3  38634  poimirlem4  38635  poimirlem17  38648  poimirlem20  38651  poimirlem24  38655  poimirlem25  38656  poimirlem29  38660  poimirlem30  38661  poimirlem31  38662  poimirlem32  38663  isrngohom  38992  islfl  40210  islpolN  42633  constmap  43817  mzpclall  43831  mzpf  43840  mzpindd  43850  mzpcompact2lem  43855  eldiophb  43861  mendring  44283  clsk1independent  45139  k0004lem3  45242  mnringmulrcld  45319  dvnprodlem3  47051  fourierdlem70  47279  fourierdlem102  47311  fourierdlem114  47323  etransclem35  47372  hoicvrrex  47659  ovnhoilem1  47704  ovnovollem2  47760  nnsum3primes4  48979  nnsum3primesprm  48981  grimfn  49070  isgrim  49073  line2  49957  line2x  49959  line2y  49960  funcf2lem  50288  aacllem  51107  crosspcld  51127  veronesematbasd  51148  veroquadmodzerod  51152  veroquadnolindfd  51153  veroquaddetzerod  51154