Theorem elmapg 8879

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 8876	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ↑m 𝐵) = {𝑔 ∣ 𝑔:𝐵⟶𝐴})
2	1	eleq2d 2827	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴}))
3		fex2 7958	. . . . 5 ⊢ ((𝐶:𝐵⟶𝐴 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 𝐶 ∈ V)
4	3	3com13 1125	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶:𝐵⟶𝐴) → 𝐶 ∈ V)
5	4	3expia 1122	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶:𝐵⟶𝐴 → 𝐶 ∈ V))
6		feq1 6716	. . . 4 ⊢ (𝑔 = 𝐶 → (𝑔:𝐵⟶𝐴 ↔ 𝐶:𝐵⟶𝐴))
7	6	elab3g 3685	. . 3 ⊢ ((𝐶:𝐵⟶𝐴 → 𝐶 ∈ V) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
8	5, 7	syl 17	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
9	2, 8	bitrd 279	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  {cab 2714  Vcvv 3480  ⟶wf 6557  (class class class)co 7431   ↑_m cmap 8866

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-map 8868

This theorem is referenced by:  elmapd  8880  mapdm0  8882  elmapi  8889  elmap  8911  map0g  8924  fdiagfn  8930  ralxpmap  8936  ixpssmap2g  8967  snmapen  9078  pw2f1olem  9116  mapxpen  9183  fseqenlem1  10064  fseqdom  10066  infpwfien  10102  fin23lem17  10378  fin23lem39  10390  isf34lem6  10420  gruurn  10838  intgru  10854  grutsk1  10861  wrdval  14555  wrdnval  14583  vdwlem4  17022  vdwlem9  17027  vdwlem10  17028  vdwlem11  17029  vdwlem13  17031  vdw  17032  vdwnnlem1  17033  rami  17053  ramcl  17067  prmgaplcm  17098  pwselbasb  17533  funcestrcsetclem7  18191  funcestrcsetclem8  18192  fullestrcsetc  18196  funcsetcestrclem8  18207  funcsetcestrclem9  18208  fullsetcestrc  18211  mndvcl  18810  gsummptnn0fz  20004  isrnghm  20441  rnghmsscmap2  20629  rnghmsscmap  20630  funcrngcsetc  20640  funcrngcsetcALT  20641  rhmsscmap2  20658  rhmsscmap  20659  funcringcsetc  20674  frlmbasf  21780  frlmsplit2  21793  uvcff  21811  psrbag  21937  evlsval2  22111  coe1fsupp  22216  gsummoncoe1  22312  evls1sca  22327  mamucl  22405  mamuvs1  22409  mamuvs2  22410  matbas2d  22429  matecl  22431  mamumat1cl  22445  mattposcl  22459  tposmap  22463  mat1dimelbas  22477  mavmulcl  22553  mdetunilem9  22626  pmatcollpw3lem  22789  pmatcollpw3fi1lem2  22793  cpmidpmatlem2  22877  cpmadumatpolylem1  22887  cayhamlem3  22893  cayhamlem4  22894  iscn  23243  iscnp  23245  cndis  23299  cnindis  23300  hausmapdom  23508  xkoptsub  23662  pt1hmeo  23814  flfval  23998  fcfval  24041  tmdgsum2  24104  symgtgp  24114  isucn  24287  ispsmet  24314  ismet  24333  isxmet  24334  imasdsf1olem  24383  elcncf  24915  metcld2  25341  elply2  26235  plyf  26237  elplyr  26240  plyeq0lem  26249  plyeq0  26250  plyaddlem  26254  plymullem  26255  dgrlem  26268  coeidlem  26276  ulmval  26423  ulmss  26440  ulmcn  26442  mtest  26447  pserulm  26465  isch2  31242  fmptco1f1o  32643  resf1o  32741  indf1ofs  32851  fedgmullem2  33681  smatrcl  33795  imambfm  34264  mbfmcnt  34270  isrrvv  34445  reprsuc  34630  reprinrn  34633  reprlt  34634  reprgt  34636  reprinfz1  34637  reprpmtf1o  34641  reprdifc  34642  circlevma  34657  deranglem  35171  indispconn  35239  prv1n  35436  knoppcnlem5  36498  knoppcnlem8  36501  curf  37605  matunitlindflem1  37623  matunitlindflem2  37624  matunitlindf  37625  fvopabf4g  37729  sdclem2  37749  sdclem1  37750  ismtyval  37807  rrncmslem  37839  aks6d1c2lem3  42127  aks6d1c5lem3  42138  aks6d1c5lem2  42139  sticksstones23  42170  evlsval3  42569  mapfzcons  42727  mzpindd  42757  mzpsubst  42759  mzprename  42760  diophrw  42770  pw2f1ocnv  43049  ofoafg  43367  snelmap  45087  fvmap  45203  difmap  45212  mapssbi  45218  fourierdlem54  46175  fourierdlem111  46232  etransclem25  46274  qndenserrnbllem  46309  elhoi  46557  hoiprodcl2  46570  hoicvrrex  46571  ovnlecvr  46573  ovn0lem  46580  hsphoif  46591  hoidmvval  46592  hsphoival  46594  hoidmvle  46615  ovnhoilem1  46616  ovnhoilem2  46617  ovnlecvr2  46625  ovncvr2  46626  hoidifhspval2  46630  hoiqssbllem3  46639  hspmbllem2  46642  opnvonmbllem1  46647  nnsum3primesgbe  47779  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  isclintop  48123  funcringcsetcALTV2lem8  48213  funcringcsetclem8ALTV  48236  ofaddmndmap  48259  mapsnop  48260  zlmodzxzel  48271  linccl  48331  lincvalsc0  48338  lcoc0  48339  linc0scn0  48340  lincdifsn  48341  linc1  48342  lincsum  48346  lincscm  48347  lincscmcl  48349  lcoss  48353  lincext1  48371  lindslinindimp2lem2  48376  lindsrng01  48385  snlindsntorlem  48387  lincresunit1  48394  lincresunit3  48398  zlmodzxzldeplem1  48417  naryfvalel  48551  1arympt1fv  48560  1arymaptfo  48564  2arymaptf  48573  prelrrx2  48634  line2x  48675  line2y  48676  map0cor  48764