Theorem elmapg 7757

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

Assertion

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

Proof of Theorem elmapg

Dummy variable 𝑔 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mapvalg 7754	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ↑𝑚 𝐵) = {𝑔 ∣ 𝑔:𝐵⟶𝐴})
2	1	eleq2d 2673	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴}))
3		fex2 7014	. . . . 5 ⊢ ((𝐶:𝐵⟶𝐴 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 𝐶 ∈ V)
4	3	3com13 1262	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶:𝐵⟶𝐴) → 𝐶 ∈ V)
5	4	3expia 1259	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶:𝐵⟶𝐴 → 𝐶 ∈ V))
6		feq1 5939	. . . 4 ⊢ (𝑔 = 𝐶 → (𝑔:𝐵⟶𝐴 ↔ 𝐶:𝐵⟶𝐴))
7	6	elab3g 3326	. . 3 ⊢ ((𝐶:𝐵⟶𝐴 → 𝐶 ∈ V) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
8	5, 7	syl 17	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
9	2, 8	bitrd 267	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐶:𝐵⟶𝐴))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∈ wcel 1977  {cab 2596  Vcvv 3173  ⟶wf 5800  (class class class)co 6549   ↑_𝑚 cmap 7744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-map 7746

This theorem is referenced by:  elmapd  7758  elmapi  7765  elmap  7772  map0e  7781  map0g  7783  fdiagfn  7787  ralxpmap  7793  ixpssmap2g  7823  map1  7921  pw2f1olem  7949  mapxpen  8011  fseqenlem1  8730  fseqdom  8732  infpwfien  8768  fin23lem17  9043  fin23lem39  9055  isf34lem6  9085  gruurn  9499  intgru  9515  grutsk1  9522  hashfacen  13095  wrdval  13163  wrdnval  13190  vdwlem4  15526  vdwlem9  15531  vdwlem10  15532  vdwlem11  15533  vdwlem13  15535  vdw  15536  vdwnnlem1  15537  rami  15557  ramcl  15571  prmgaplcm  15602  pwselbasb  15971  elestrchom  16591  estrcco  16593  funcestrcsetclem7  16609  funcestrcsetclem8  16610  fullestrcsetc  16614  funcsetcestrclem7  16624  funcsetcestrclem8  16625  funcsetcestrclem9  16626  fullsetcestrc  16629  symgbas  17623  gsummptnn0fz  18205  psrbag  19185  evlsval2  19341  coe1fsupp  19405  gsummoncoe1  19495  evls1sca  19509  frlmbasf  19923  frlmsplit2  19931  uvcff  19949  mndvcl  20016  mamucl  20026  mamuvs1  20030  mamuvs2  20031  matbas2d  20048  matecl  20050  mamumat1cl  20064  mattposcl  20078  tposmap  20082  mat1dimelbas  20096  mavmulcl  20172  mdetunilem9  20245  pmatcollpw3lem  20407  pmatcollpw3fi1lem2  20411  cpmidpmatlem2  20495  cpmadumatpolylem1  20505  cayhamlem3  20511  cayhamlem4  20512  iscn  20849  iscnp  20851  cndis  20905  cnindis  20906  hausmapdom  21113  xkoptsub  21267  pt1hmeo  21419  flfval  21604  fcfval  21647  tmdgsum2  21710  symgtgp  21715  isucn  21892  ispsmet  21919  ismet  21938  isxmet  21939  imasdsf1olem  21988  elcncf  22500  metcld2  22913  elply2  23756  plyf  23758  elplyr  23761  plyeq0lem  23770  plyeq0  23771  plyaddlem  23775  plymullem  23776  dgrlem  23789  coeidlem  23797  ulmval  23938  ulmss  23955  ulmcn  23957  mtest  23962  pserulm  23980  isch2  27464  resf1o  28893  smatrcl  29190  indf1ofs  29415  imambfm  29651  mbfmcnt  29657  isrrvv  29832  deranglem  30402  indispcon  30470  knoppcnlem5  31657  knoppcnlem8  31660  curf  32557  matunitlindflem1  32575  matunitlindflem2  32576  matunitlindf  32577  fvopabf4g  32685  sdclem2  32708  sdclem1  32709  ismtyval  32769  rrncmslem  32801  mapfzcons  36297  mzpindd  36327  mzpsubst  36329  mzprename  36330  diophrw  36340  pw2f1ocnv  36622  snelmap  38280  mapdm0  38378  fvmap  38382  mapsnd  38383  difmap  38394  mapssbi  38400  fourierdlem54  39053  fourierdlem111  39110  etransclem25  39152  qndenserrnbllem  39190  elhoi  39432  hoiprodcl2  39445  hoicvrrex  39446  ovnlecvr  39448  ovn0lem  39455  hsphoif  39466  hoidmvval  39467  hsphoival  39469  hoidmvle  39490  ovnhoilem1  39491  ovnhoilem2  39492  ovnlecvr2  39500  ovncvr2  39501  hoidifhspval2  39505  hoiqssbllem3  39514  hspmbllem2  39517  opnvonmbllem1  39522  nnsum3primesgbe  40208  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  isclintop  41633  isrnghm  41682  rnghmsscmap2  41765  rnghmsscmap  41766  funcrngcsetc  41790  funcrngcsetcALT  41791  rhmsscmap2  41811  rhmsscmap  41812  funcringcsetc  41827  funcringcsetcALTV2lem8  41835  funcringcsetclem8ALTV  41858  ofaddmndmap  41915  mapsnop  41916  mapprop  41917  zlmodzxzel  41926  linccl  41997  lincvalsc0  42004  lcoc0  42005  linc0scn0  42006  lincdifsn  42007  linc1  42008  lincsum  42012  lincscm  42013  lincscmcl  42015  lcoss  42019  lincext1  42037  lindslinindimp2lem2  42042  lindsrng01  42051  snlindsntorlem  42053  lincresunit1  42060  lincresunit3  42064  zlmodzxzldeplem1  42083