Theorem elmap 8900

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 8860	. 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 8848

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 4584  df-pr 4586  df-op 4590  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 8850

This theorem is used by:  mapval2  8901  fvmptmap  8910  mapsnconst  8921  mapsncnv  8922  xpmapenlem  9164  pwfseqlem3  10746  tskcard  10867  ingru  10901  rpnnen1lem1  13107  rpnnen1lem3  13108  rpnnen1lem4  13109  rpnnen1lem5  13110  facmapnn  14430  prmreclem2  17096  1arith  17106  vdwlem6  17165  vdwlem7  17166  vdwlem8  17167  vdwlem9  17168  vdwlem11  17170  vdwlem13  17172  prmgapprmo  17241  isfunc  18040  isfuncd  18041  idfucl  18057  cofucl  18064  funcres2b  18073  wunfunc  18077  catcfuccl  18294  funcestrcsetclem9  18323  ismgmhm  18886  ismhm  18981  efmnd1bas  19090  smndex1ibas  19097  smndex1gbas  19099  smndex1gbasOLD  19100  dfrhm2  20705  isrhm0  20707  isabv  21069  pjdm  22014  pjfval2  22016  psrelbas  22244  psraddcl  22248  psrmulcllem  22254  psrvscacl  22260  psr0cl  22261  psrnegcl  22263  psr1cl  22269  subrgpsr  22286  mvrf  22293  mplmon  22345  mplcoe1  22347  coe1fval3  22527  00ply1bas  22558  ply1plusgfvi  22560  coe1z  22583  coe1mul2  22589  coe1tm  22593  pnrmopn  23662  distgp  24419  indistgp  24420  ehl1eudis  25742  ehl2eudis  25744  elovolmlem  25796  itg2seq  26064  coeeulem  26544  coeeq  26547  aannenlem1  26656  dvntaylp  26699  taylthlem1  26701  taylthlem2  26702  pserdvlem2  26756  lgamgulmlem6  27362  sqff1o  27510  isismt  28998  elee  29472  islno  31356  nmooval  31366  ajfval  31412  h2hcau  31582  h2hlm  31583  hcau  31787  hlimadd  31796  hhcms  31806  hlim0  31838  hhsscms  31881  pjmf1  32319  hosmval  32338  hommval  32339  hodmval  32340  hfsmval  32341  hfmmval  32342  elcnop  32460  ellnop  32461  elhmop  32476  hmopex  32478  nlfnval  32484  elcnfn  32485  ellnfn  32486  dmadjss  32490  dmadjop  32491  adjeu  32492  adjval  32493  hhcno  32507  hhcnf  32508  adjbdln  32686  isst  32816  ishst  32817  maprnin  33366  fpwrelmap  33368  fpwrelmapffs  33369  ismnt  33587  mgcval  33591  fply1  34133  psrmon  34224  zarcmplem  34556  eulerpartleme  35038  eulerpartlemt  35046  eulerpartlemr  35049  eulerpartlemmf  35050  eulerpartlemgvv  35051  eulerpartlemgs2  35055  eulerpartlemn  35056  reprinfz1  35294  breprexplemb  35303  breprexpnat  35306  vtsval  35309  circlemethnat  35313  circlemethhgt  35315  ex-sategoelel12  36261  mrsubff  36346  mrsubrn  36347  msubff  36364  poimirlem3  38617  poimirlem4  38618  poimirlem17  38631  poimirlem20  38634  poimirlem24  38638  poimirlem25  38639  poimirlem29  38643  poimirlem30  38644  poimirlem31  38645  poimirlem32  38646  isrngohom  38975  islfl  40193  islpolN  42616  constmap  43800  mzpclall  43814  mzpf  43823  mzpindd  43833  mzpcompact2lem  43838  eldiophb  43844  mendring  44266  clsk1independent  45122  k0004lem3  45225  mnringmulrcld  45302  dvnprodlem3  47034  fourierdlem70  47262  fourierdlem102  47294  fourierdlem114  47306  etransclem35  47355  hoicvrrex  47642  ovnhoilem1  47687  ovnovollem2  47743  nnsum3primes4  48962  nnsum3primesprm  48964  grimfn  49053  isgrim  49056  rrx2xpref1o  49906  rrx2linesl  49931  line2  49940  line2x  49942  line2y  49943  funcf2lem  50265  aacllem  51015  crosspcld  51035  veronesematbasd  51056  veroquadmodzerod  51060  veroquadnolindfd  51061  veroquaddetzerod  51062