Theorem elmapg 8887

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 8884	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ↑m 𝐵) = {𝑔 ∣ 𝑔:𝐵⟶𝐴})
2	1	eleq2d 2850	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴}))
3		fex2 7972	. . . . 5 ⊢ ((𝐶:𝐵⟶𝐴 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 𝐶 ∈ V)
4	3	3com13 1142	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶:𝐵⟶𝐴) → 𝐶 ∈ V)
5	4	3expia 1139	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶:𝐵⟶𝐴 → 𝐶 ∈ V))
6		feq1 6709	. . . 4 ⊢ (𝑔 = 𝐶 → (𝑔:𝐵⟶𝐴 ↔ 𝐶:𝐵⟶𝐴))
7	6	elab3g 3642	. . 3 ⊢ ((𝐶:𝐵⟶𝐴 → 𝐶 ∈ V) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
8	5, 7	syl 18	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
9	2, 8	bitrd 282	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2147  {cab 2741  Vcvv 3454  ⟶wf 6554  (class class class)co 7443   ↑_m cmap 8875

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-pow 5331  ax-pr 5395  ax-un 7775

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-fv 6566  df-ov 7446  df-oprab 7447  df-mpo 7448  df-map 8877

This theorem is used by:  elmapd  8888  mapdm0  8890  elmapi  8897  curf  8918  elmap  8927  map0g  8940  fdiagfn  8946  ralxpmap  8952  ixpssmap2g  8983  snmapen  9094  pw2f1olem  9128  mapxpen  9190  fseqenlem1  10130  fseqdom  10132  infpwfien  10168  fin23lem17  10443  fin23lem39  10455  isf34lem6  10485  gruurn  10910  intgru  10926  grutsk1  10933  wrdval  14688  wrdnval  14717  vdwlem4  17191  vdwlem9  17196  vdwlem10  17197  vdwlem11  17198  vdwlem13  17200  vdw  17201  vdwnnlem1  17202  rami  17222  ramcl  17236  prmgaplcm  17267  pwselbasb  17688  funcestrcsetclem7  18349  funcestrcsetclem8  18350  fullestrcsetc  18354  funcsetcestrclem8  18365  funcsetcestrclem9  18366  fullsetcestrc  18369  mndvcl  19021  gsummptnn0fz  20230  isrnghm  20701  rnghmsscmap2  20911  rnghmsscmap  20912  funcrngcsetc  20922  funcrngcsetcALT  20923  rhmsscmap2  20940  rhmsscmap  20941  funcringcsetc  20956  frlmbasf  22096  frlmsplit2  22109  uvcff  22127  psrbag  22255  evlsval2  22426  evlsval3  22428  coe1fsupp  22562  gsummoncoe1  22656  evls1sca  22671  mamucl  22746  mamuvs1  22750  mamuvs2  22751  matbas2d  22768  matecl  22770  mamumat1cl  22784  mattposcl  22798  tposmap  22802  mat1dimelbas  22816  mavmulcl  22892  mdetunilem9  22965  matunitlindflem1  23024  matunitlindflem2  23025  matunitlindf  23026  pmatcollpw3lem  23131  pmatcollpw3fi1lem2  23135  cpmidpmatlem2  23219  cpmadumatpolylem1  23229  cayhamlem3  23235  cayhamlem4  23236  iscn  23583  iscnp  23585  cndis  23639  cnindis  23640  hausmapdom  23849  xkoptsub  24003  pt1hmeo  24155  flfval  24339  fcfval  24382  tmdgsum2  24445  symgtgp  24455  isucn  24626  ispsmet  24653  ismet  24672  isxmet  24673  imasdsf1olem  24722  elcncf  25240  metcld2  25658  elply2  26544  plyf  26546  elplyr  26549  plyeq0lem  26559  plyeq0  26560  plyaddlem  26564  plymullem  26565  dgrlem  26578  coeidlem  26586  ulmval  26737  ulmss  26754  ulmcn  26756  mtest  26761  pserulm  26779  isch2  31855  fmptco1f1o  33299  resf1o  33392  indf1ofs  33503  fedgmullem2  34332  smatrcl  34498  imambfm  34964  mbfmcnt  34970  isrrvv  35145  reprsuc  35314  reprinrn  35317  reprlt  35318  reprgt  35320  reprinfz1  35321  reprpmtf1o  35325  reprdifc  35326  circlevma  35341  deranglem  36098  indispconn  36166  prv1n  36363  knoppcnlem5  37541  knoppcnlem8  37544  fvopabf4g  38848  sdclem2  38868  sdclem1  38869  ismtyval  38926  rrncmslem  38958  aks6d1c2lem3  43368  aks6d1c5lem3  43379  aks6d1c5lem2  43380  sticksstones23  43411  mapfzcons  43920  mzpindd  43950  mzpsubst  43952  mzprename  43953  diophrw  43963  pw2f1ocnv  44237  ofoafg  44548  snelmap  46304  fvmap  46417  difmap  46425  mapssbi  46431  fourierdlem54  47375  fourierdlem111  47432  etransclem25  47474  qndenserrnbllem  47509  elhoi  47757  hoiprodcl2  47770  hoicvrrex  47771  ovnlecvr  47773  ovn0lem  47780  hsphoif  47791  hoidmvval  47792  hsphoival  47794  hoidmvle  47815  ovnhoilem1  47816  ovnhoilem2  47817  ovnlecvr2  47825  ovncvr2  47826  hoidifhspval2  47830  hoiqssbllem3  47839  hspmbllem2  47842  opnvonmbllem1  47847  nnsum3primesgbe  49095  nnsum4primesodd  49099  nnsum4primesoddALTV  49100  nnsum4primeseven  49103  nnsum4primesevenALTV  49104  isclintop  49509  funcringcsetcALTV2lem8  49599  funcringcsetclem8ALTV  49622  ofaddmndmap  49660  mapsnop  49661  zlmodzxzel  49672  linccl  49731  lincvalsc0  49738  lcoc0  49739  linc0scn0  49740  lincdifsn  49741  linc1  49742  lincsum  49746  lincscm  49747  lincscmcl  49749  lcoss  49753  lincext1  49771  lindslinindimp2lem2  49776  lindsrng01  49785  snlindsntorlem  49787  lincresunit1  49794  lincresunit3  49798  zlmodzxzldeplem1  49817  naryfvalel  49947  1arympt1fv  49956  1arymaptfo  49960  2arymaptf  49969  line2x  50071  line2y  50072  map0cor  50171