Theorem elmapg 8776

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 8773	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ↑m 𝐵) = {𝑔 ∣ 𝑔:𝐵⟶𝐴})
2	1	eleq2d 2822	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴}))
3		fex2 7878	. . . . 5 ⊢ ((𝐶:𝐵⟶𝐴 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 𝐶 ∈ V)
4	3	3com13 1124	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶:𝐵⟶𝐴) → 𝐶 ∈ V)
5	4	3expia 1121	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶:𝐵⟶𝐴 → 𝐶 ∈ V))
6		feq1 6640	. . . 4 ⊢ (𝑔 = 𝐶 → (𝑔:𝐵⟶𝐴 ↔ 𝐶:𝐵⟶𝐴))
7	6	elab3g 3640	. . 3 ⊢ ((𝐶:𝐵⟶𝐴 → 𝐶 ∈ V) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
8	5, 7	syl 17	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
9	2, 8	bitrd 279	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2113  {cab 2714  Vcvv 3440  ⟶wf 6488  (class class class)co 7358   ↑_m cmap 8763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7361  df-oprab 7362  df-mpo 7363  df-map 8765

This theorem is referenced by:  elmapd  8777  mapdm0  8779  elmapi  8786  elmap  8809  map0g  8822  fdiagfn  8828  ralxpmap  8834  ixpssmap2g  8865  snmapen  8975  pw2f1olem  9009  mapxpen  9071  fseqenlem1  9934  fseqdom  9936  infpwfien  9972  fin23lem17  10248  fin23lem39  10260  isf34lem6  10290  gruurn  10709  intgru  10725  grutsk1  10732  wrdval  14439  wrdnval  14468  vdwlem4  16912  vdwlem9  16917  vdwlem10  16918  vdwlem11  16919  vdwlem13  16921  vdw  16922  vdwnnlem1  16923  rami  16943  ramcl  16957  prmgaplcm  16988  pwselbasb  17408  funcestrcsetclem7  18069  funcestrcsetclem8  18070  fullestrcsetc  18074  funcsetcestrclem8  18085  funcsetcestrclem9  18086  fullsetcestrc  18089  mndvcl  18722  gsummptnn0fz  19915  isrnghm  20377  rnghmsscmap2  20562  rnghmsscmap  20563  funcrngcsetc  20573  funcrngcsetcALT  20574  rhmsscmap2  20591  rhmsscmap  20592  funcringcsetc  20607  frlmbasf  21715  frlmsplit2  21728  uvcff  21746  psrbag  21873  evlsval2  22042  evlsval3  22044  coe1fsupp  22155  gsummoncoe1  22252  evls1sca  22267  mamucl  22345  mamuvs1  22349  mamuvs2  22350  matbas2d  22367  matecl  22369  mamumat1cl  22383  mattposcl  22397  tposmap  22401  mat1dimelbas  22415  mavmulcl  22491  mdetunilem9  22564  pmatcollpw3lem  22727  pmatcollpw3fi1lem2  22731  cpmidpmatlem2  22815  cpmadumatpolylem1  22825  cayhamlem3  22831  cayhamlem4  22832  iscn  23179  iscnp  23181  cndis  23235  cnindis  23236  hausmapdom  23444  xkoptsub  23598  pt1hmeo  23750  flfval  23934  fcfval  23977  tmdgsum2  24040  symgtgp  24050  isucn  24221  ispsmet  24248  ismet  24267  isxmet  24268  imasdsf1olem  24317  elcncf  24838  metcld2  25263  elply2  26157  plyf  26159  elplyr  26162  plyeq0lem  26171  plyeq0  26172  plyaddlem  26176  plymullem  26177  dgrlem  26190  coeidlem  26198  ulmval  26345  ulmss  26362  ulmcn  26364  mtest  26369  pserulm  26387  isch2  31298  fmptco1f1o  32711  resf1o  32809  indf1ofs  32948  fedgmullem2  33787  smatrcl  33953  imambfm  34419  mbfmcnt  34425  isrrvv  34600  reprsuc  34772  reprinrn  34775  reprlt  34776  reprgt  34778  reprinfz1  34779  reprpmtf1o  34783  reprdifc  34784  circlevma  34799  deranglem  35360  indispconn  35428  prv1n  35625  knoppcnlem5  36697  knoppcnlem8  36700  curf  37795  matunitlindflem1  37813  matunitlindflem2  37814  matunitlindf  37815  fvopabf4g  37919  sdclem2  37939  sdclem1  37940  ismtyval  37997  rrncmslem  38029  aks6d1c2lem3  42376  aks6d1c5lem3  42387  aks6d1c5lem2  42388  sticksstones23  42419  mapfzcons  42954  mzpindd  42984  mzpsubst  42986  mzprename  42987  diophrw  42997  pw2f1ocnv  43275  ofoafg  43592  snelmap  45323  fvmap  45438  difmap  45447  mapssbi  45453  fourierdlem54  46400  fourierdlem111  46457  etransclem25  46499  qndenserrnbllem  46534  elhoi  46782  hoiprodcl2  46795  hoicvrrex  46796  ovnlecvr  46798  ovn0lem  46805  hsphoif  46816  hoidmvval  46817  hsphoival  46819  hoidmvle  46840  ovnhoilem1  46841  ovnhoilem2  46842  ovnlecvr2  46850  ovncvr2  46851  hoidifhspval2  46855  hoiqssbllem3  46864  hspmbllem2  46867  opnvonmbllem1  46872  nnsum3primesgbe  48034  nnsum4primesodd  48038  nnsum4primesoddALTV  48039  nnsum4primeseven  48042  nnsum4primesevenALTV  48043  isclintop  48449  funcringcsetcALTV2lem8  48539  funcringcsetclem8ALTV  48562  ofaddmndmap  48585  mapsnop  48586  zlmodzxzel  48597  linccl  48656  lincvalsc0  48663  lcoc0  48664  linc0scn0  48665  lincdifsn  48666  linc1  48667  lincsum  48671  lincscm  48672  lincscmcl  48674  lcoss  48678  lincext1  48696  lindslinindimp2lem2  48701  lindsrng01  48710  snlindsntorlem  48712  lincresunit1  48719  lincresunit3  48723  zlmodzxzldeplem1  48742  naryfvalel  48872  1arympt1fv  48881  1arymaptfo  48885  2arymaptf  48894  prelrrx2  48955  line2x  48996  line2y  48997  map0cor  49096