Theorem elmapg 8586

Description: Membership relation for set exponentiation. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 15-Nov-2014.)

Assertion

Ref	Expression
elmapg	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴))

Proof of Theorem elmapg

Dummy variable 𝑔 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mapvalg 8583	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ↑m 𝐵) = {𝑔 ∣ 𝑔:𝐵⟶𝐴})
2	1	eleq2d 2824	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴}))
3		fex2 7754	. . . . 5 ⊢ ((𝐶:𝐵⟶𝐴 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 𝐶 ∈ V)
4	3	3com13 1122	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶:𝐵⟶𝐴) → 𝐶 ∈ V)
5	4	3expia 1119	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶:𝐵⟶𝐴 → 𝐶 ∈ V))
6		feq1 6565	. . . 4 ⊢ (𝑔 = 𝐶 → (𝑔:𝐵⟶𝐴 ↔ 𝐶:𝐵⟶𝐴))
7	6	elab3g 3609	. . 3 ⊢ ((𝐶:𝐵⟶𝐴 → 𝐶 ∈ V) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
8	5, 7	syl 17	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
9	2, 8	bitrd 278	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∈ wcel 2108  {cab 2715  Vcvv 3422  ⟶wf 6414  (class class class)co 7255   ↑_m cmap 8573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-map 8575

This theorem is referenced by:  elmapd  8587  mapdm0  8588  elmapi  8595  elmap  8617  map0g  8630  fdiagfn  8636  ralxpmap  8642  ixpssmap2g  8673  snmapen  8782  pw2f1olem  8816  mapxpen  8879  fseqenlem1  9711  fseqdom  9713  infpwfien  9749  fin23lem17  10025  fin23lem39  10037  isf34lem6  10067  gruurn  10485  intgru  10501  grutsk1  10508  hashfacenOLD  14095  wrdval  14148  wrdnval  14176  vdwlem4  16613  vdwlem9  16618  vdwlem10  16619  vdwlem11  16620  vdwlem13  16622  vdw  16623  vdwnnlem1  16624  rami  16644  ramcl  16658  prmgaplcm  16689  pwselbasb  17116  funcestrcsetclem7  17779  funcestrcsetclem8  17780  fullestrcsetc  17784  funcsetcestrclem8  17795  funcsetcestrclem9  17796  fullsetcestrc  17799  gsummptnn0fz  19502  frlmbasf  20877  frlmsplit2  20890  uvcff  20908  psrbag  21030  evlsval2  21207  coe1fsupp  21295  gsummoncoe1  21385  evls1sca  21399  mndvcl  21450  mamucl  21458  mamuvs1  21462  mamuvs2  21463  matbas2d  21480  matecl  21482  mamumat1cl  21496  mattposcl  21510  tposmap  21514  mat1dimelbas  21528  mavmulcl  21604  mdetunilem9  21677  pmatcollpw3lem  21840  pmatcollpw3fi1lem2  21844  cpmidpmatlem2  21928  cpmadumatpolylem1  21938  cayhamlem3  21944  cayhamlem4  21945  iscn  22294  iscnp  22296  cndis  22350  cnindis  22351  hausmapdom  22559  xkoptsub  22713  pt1hmeo  22865  flfval  23049  fcfval  23092  tmdgsum2  23155  symgtgp  23165  isucn  23338  ispsmet  23365  ismet  23384  isxmet  23385  imasdsf1olem  23434  elcncf  23958  metcld2  24376  elply2  25262  plyf  25264  elplyr  25267  plyeq0lem  25276  plyeq0  25277  plyaddlem  25281  plymullem  25282  dgrlem  25295  coeidlem  25303  ulmval  25444  ulmss  25461  ulmcn  25463  mtest  25468  pserulm  25486  isch2  29486  fmptco1f1o  30869  resf1o  30967  fedgmullem2  31613  smatrcl  31648  indf1ofs  31894  imambfm  32129  mbfmcnt  32135  isrrvv  32310  reprsuc  32495  reprinrn  32498  reprlt  32499  reprgt  32501  reprinfz1  32502  reprpmtf1o  32506  reprdifc  32507  circlevma  32522  deranglem  33028  indispconn  33096  prv1n  33293  knoppcnlem5  34604  knoppcnlem8  34607  curf  35682  matunitlindflem1  35700  matunitlindflem2  35701  matunitlindf  35702  fvopabf4g  35806  sdclem2  35827  sdclem1  35828  ismtyval  35885  rrncmslem  35917  evlsval3  40195  mapfzcons  40454  mzpindd  40484  mzpsubst  40486  mzprename  40487  diophrw  40497  pw2f1ocnv  40775  snelmap  42521  fvmap  42626  difmap  42636  mapssbi  42642  fourierdlem54  43591  fourierdlem111  43648  etransclem25  43690  qndenserrnbllem  43725  elhoi  43970  hoiprodcl2  43983  hoicvrrex  43984  ovnlecvr  43986  ovn0lem  43993  hsphoif  44004  hoidmvval  44005  hsphoival  44007  hoidmvle  44028  ovnhoilem1  44029  ovnhoilem2  44030  ovnlecvr2  44038  ovncvr2  44039  hoidifhspval2  44043  hoiqssbllem3  44052  hspmbllem2  44055  opnvonmbllem1  44060  nnsum3primesgbe  45132  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  isclintop  45289  isrnghm  45338  rnghmsscmap2  45419  rnghmsscmap  45420  funcrngcsetc  45444  funcrngcsetcALT  45445  rhmsscmap2  45465  rhmsscmap  45466  funcringcsetc  45481  funcringcsetcALTV2lem8  45489  funcringcsetclem8ALTV  45512  ofaddmndmap  45567  mapsnop  45568  zlmodzxzel  45579  linccl  45643  lincvalsc0  45650  lcoc0  45651  linc0scn0  45652  lincdifsn  45653  linc1  45654  lincsum  45658  lincscm  45659  lincscmcl  45661  lcoss  45665  lincext1  45683  lindslinindimp2lem2  45688  lindsrng01  45697  snlindsntorlem  45699  lincresunit1  45706  lincresunit3  45710  zlmodzxzldeplem1  45729  naryfvalel  45864  1arympt1fv  45873  1arymaptfo  45877  2arymaptf  45886  prelrrx2  45947  line2x  45988  line2y  45989  map0cor  46070