Theorem elmap 8878

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2146  Vcvv 3458  ⟶wf 6539  (class class class)co 7423   ↑_m cmap 8833

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-pow 5341  ax-pr 5409  ax-un 7745

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7426  df-oprab 7427  df-mpo 7428  df-map 8835

This theorem is used by:  mapval2  8879  fvmptmap  8888  mapsnconst  8899  mapsncnv  8900  xpmapenlem  9142  pwfseqlem3  10663  tskcard  10784  ingru  10818  rpnnen1lem1  13020  rpnnen1lem3  13021  rpnnen1lem4  13022  rpnnen1lem5  13023  facmapnn  14341  prmreclem2  17002  1arith  17012  vdwlem6  17071  vdwlem7  17072  vdwlem8  17073  vdwlem9  17074  vdwlem11  17076  vdwlem13  17078  prmgapprmo  17147  isfunc  17946  isfuncd  17947  idfucl  17963  cofucl  17970  funcres2b  17979  wunfunc  17983  catcfuccl  18200  funcestrcsetclem9  18229  ismgmhm  18783  ismhm  18874  efmnd1bas  18983  smndex1ibas  18990  smndex1gbas  18992  smndex1gbasOLD  18993  dfrhm2  20589  isrhm0  20591  isabv  20951  pjdm  21894  pjfval2  21896  psrelbas  22122  psraddcl  22126  psrmulcllem  22132  psrvscacl  22138  psr0cl  22139  psrnegcl  22141  psr1cl  22147  subrgpsr  22164  mvrf  22171  mplmon  22223  mplcoe1  22225  coe1fval3  22405  00ply1bas  22436  ply1plusgfvi  22438  coe1z  22461  coe1mul2  22467  coe1tm  22471  pnrmopn  23537  distgp  24293  indistgp  24294  ehl1eudis  25616  ehl2eudis  25618  elovolmlem  25670  itg2seq  25938  coeeulem  26418  coeeq  26421  aannenlem1  26528  dvntaylp  26571  taylthlem1  26573  taylthlem2  26574  pserdvlem2  26628  lgamgulmlem6  27235  sqff1o  27383  isismt  28840  elee  29280  islno  31142  nmooval  31152  ajfval  31198  h2hcau  31368  h2hlm  31369  hcau  31573  hlimadd  31582  hhcms  31592  hlim0  31624  hhsscms  31667  pjmf1  32105  hosmval  32124  hommval  32125  hodmval  32126  hfsmval  32127  hfmmval  32128  elcnop  32246  ellnop  32247  elhmop  32262  hmopex  32264  nlfnval  32270  elcnfn  32271  ellnfn  32272  dmadjss  32276  dmadjop  32277  adjeu  32278  adjval  32279  hhcno  32293  hhcnf  32294  adjbdln  32472  isst  32602  ishst  32603  maprnin  33113  fpwrelmap  33115  fpwrelmapffs  33116  ismnt  33334  mgcval  33338  fply1  33879  psrmon  33970  zarcmplem  34302  eulerpartleme  34784  eulerpartlemt  34792  eulerpartlemr  34795  eulerpartlemmf  34796  eulerpartlemgvv  34797  eulerpartlemgs2  34801  eulerpartlemn  34802  reprinfz1  35040  breprexplemb  35049  breprexpnat  35052  vtsval  35055  circlemethnat  35059  circlemethhgt  35061  ex-sategoelel12  35939  mrsubff  36024  mrsubrn  36025  msubff  36042  poimirlem3  38314  poimirlem4  38315  poimirlem17  38328  poimirlem20  38331  poimirlem24  38335  poimirlem25  38336  poimirlem29  38340  poimirlem30  38341  poimirlem31  38342  poimirlem32  38343  isrngohom  38656  islfl  39874  islpolN  42297  constmap  43484  mzpclall  43498  mzpf  43507  mzpindd  43517  mzpcompact2lem  43522  eldiophb  43528  mendring  43955  clsk1independent  44812  k0004lem3  44915  mnringmulrcld  44992  dvnprodlem3  46702  fourierdlem70  46930  fourierdlem102  46962  fourierdlem114  46974  etransclem35  47023  hoicvrrex  47310  ovnhoilem1  47355  ovnovollem2  47411  nnsum3primes4  48593  nnsum3primesprm  48595  grimfn  48684  isgrim  48687  rrx2xpref1o  49538  rrx2linesl  49563  line2  49572  line2x  49574  line2y  49575  funcf2lem  49899  aacllem  50661  crosspcli  50681