Theorem elmapg 8815

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  {cab 2708  Vcvv 3450  ⟶wf 6510  (class class class)co 7390   ↑_m cmap 8802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-map 8804

This theorem is referenced by:  elmapd  8816  mapdm0  8818  elmapi  8825  elmap  8847  map0g  8860  fdiagfn  8866  ralxpmap  8872  ixpssmap2g  8903  snmapen  9012  pw2f1olem  9050  mapxpen  9113  fseqenlem1  9984  fseqdom  9986  infpwfien  10022  fin23lem17  10298  fin23lem39  10310  isf34lem6  10340  gruurn  10758  intgru  10774  grutsk1  10781  wrdval  14488  wrdnval  14517  vdwlem4  16962  vdwlem9  16967  vdwlem10  16968  vdwlem11  16969  vdwlem13  16971  vdw  16972  vdwnnlem1  16973  rami  16993  ramcl  17007  prmgaplcm  17038  pwselbasb  17458  funcestrcsetclem7  18114  funcestrcsetclem8  18115  fullestrcsetc  18119  funcsetcestrclem8  18130  funcsetcestrclem9  18131  fullsetcestrc  18134  mndvcl  18731  gsummptnn0fz  19923  isrnghm  20357  rnghmsscmap2  20545  rnghmsscmap  20546  funcrngcsetc  20556  funcrngcsetcALT  20557  rhmsscmap2  20574  rhmsscmap  20575  funcringcsetc  20590  frlmbasf  21676  frlmsplit2  21689  uvcff  21707  psrbag  21833  evlsval2  22001  coe1fsupp  22106  gsummoncoe1  22202  evls1sca  22217  mamucl  22295  mamuvs1  22299  mamuvs2  22300  matbas2d  22317  matecl  22319  mamumat1cl  22333  mattposcl  22347  tposmap  22351  mat1dimelbas  22365  mavmulcl  22441  mdetunilem9  22514  pmatcollpw3lem  22677  pmatcollpw3fi1lem2  22681  cpmidpmatlem2  22765  cpmadumatpolylem1  22775  cayhamlem3  22781  cayhamlem4  22782  iscn  23129  iscnp  23131  cndis  23185  cnindis  23186  hausmapdom  23394  xkoptsub  23548  pt1hmeo  23700  flfval  23884  fcfval  23927  tmdgsum2  23990  symgtgp  24000  isucn  24172  ispsmet  24199  ismet  24218  isxmet  24219  imasdsf1olem  24268  elcncf  24789  metcld2  25214  elply2  26108  plyf  26110  elplyr  26113  plyeq0lem  26122  plyeq0  26123  plyaddlem  26127  plymullem  26128  dgrlem  26141  coeidlem  26149  ulmval  26296  ulmss  26313  ulmcn  26315  mtest  26320  pserulm  26338  isch2  31159  fmptco1f1o  32564  resf1o  32660  indf1ofs  32796  fedgmullem2  33633  smatrcl  33793  imambfm  34260  mbfmcnt  34266  isrrvv  34441  reprsuc  34613  reprinrn  34616  reprlt  34617  reprgt  34619  reprinfz1  34620  reprpmtf1o  34624  reprdifc  34625  circlevma  34640  deranglem  35160  indispconn  35228  prv1n  35425  knoppcnlem5  36492  knoppcnlem8  36495  curf  37599  matunitlindflem1  37617  matunitlindflem2  37618  matunitlindf  37619  fvopabf4g  37723  sdclem2  37743  sdclem1  37744  ismtyval  37801  rrncmslem  37833  aks6d1c2lem3  42121  aks6d1c5lem3  42132  aks6d1c5lem2  42133  sticksstones23  42164  evlsval3  42554  mapfzcons  42711  mzpindd  42741  mzpsubst  42743  mzprename  42744  diophrw  42754  pw2f1ocnv  43033  ofoafg  43350  snelmap  45083  fvmap  45199  difmap  45208  mapssbi  45214  fourierdlem54  46165  fourierdlem111  46222  etransclem25  46264  qndenserrnbllem  46299  elhoi  46547  hoiprodcl2  46560  hoicvrrex  46561  ovnlecvr  46563  ovn0lem  46570  hsphoif  46581  hoidmvval  46582  hsphoival  46584  hoidmvle  46605  ovnhoilem1  46606  ovnhoilem2  46607  ovnlecvr2  46615  ovncvr2  46616  hoidifhspval2  46620  hoiqssbllem3  46629  hspmbllem2  46632  opnvonmbllem1  46637  nnsum3primesgbe  47797  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  isclintop  48199  funcringcsetcALTV2lem8  48289  funcringcsetclem8ALTV  48312  ofaddmndmap  48335  mapsnop  48336  zlmodzxzel  48347  linccl  48407  lincvalsc0  48414  lcoc0  48415  linc0scn0  48416  lincdifsn  48417  linc1  48418  lincsum  48422  lincscm  48423  lincscmcl  48425  lcoss  48429  lincext1  48447  lindslinindimp2lem2  48452  lindsrng01  48461  snlindsntorlem  48463  lincresunit1  48470  lincresunit3  48474  zlmodzxzldeplem1  48493  naryfvalel  48623  1arympt1fv  48632  1arymaptfo  48636  2arymaptf  48645  prelrrx2  48706  line2x  48747  line2y  48748  map0cor  48847