Theorem elmapg 8843

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 8840	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ↑m 𝐵) = {𝑔 ∣ 𝑔:𝐵⟶𝐴})
2	1	eleq2d 2847	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴}))
3		fex2 7937	. . . . 5 ⊢ ((𝐶:𝐵⟶𝐴 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 𝐶 ∈ V)
4	3	3com13 1142	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶:𝐵⟶𝐴) → 𝐶 ∈ V)
5	4	3expia 1139	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶:𝐵⟶𝐴 → 𝐶 ∈ V))
6		feq1 6679	. . . 4 ⊢ (𝑔 = 𝐶 → (𝑔:𝐵⟶𝐴 ↔ 𝐶:𝐵⟶𝐴))
7	6	elab3g 3639	. . 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 2145  {cab 2739  Vcvv 3451  ⟶wf 6527  (class class class)co 7412   ↑_m cmap 8831

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7740

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 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-fv 6539  df-ov 7415  df-oprab 7416  df-mpo 7417  df-map 8833

This theorem is used by:  elmapd  8844  mapdm0  8846  elmapi  8853  curf  8874  elmap  8883  map0g  8896  fdiagfn  8902  ralxpmap  8908  ixpssmap2g  8939  snmapen  9050  pw2f1olem  9084  mapxpen  9146  fseqenlem1  10084  fseqdom  10086  infpwfien  10122  fin23lem17  10397  fin23lem39  10409  isf34lem6  10439  gruurn  10864  intgru  10880  grutsk1  10887  wrdval  14641  wrdnval  14670  vdwlem4  17142  vdwlem9  17147  vdwlem10  17148  vdwlem11  17149  vdwlem13  17151  vdw  17152  vdwnnlem1  17153  rami  17173  ramcl  17187  prmgaplcm  17218  pwselbasb  17639  funcestrcsetclem7  18300  funcestrcsetclem8  18301  fullestrcsetc  18305  funcsetcestrclem8  18316  funcsetcestrclem9  18317  fullsetcestrc  18320  mndvcl  18972  gsummptnn0fz  20180  isrnghm  20651  rnghmsscmap2  20861  rnghmsscmap  20862  funcrngcsetc  20872  funcrngcsetcALT  20873  rhmsscmap2  20890  rhmsscmap  20891  funcringcsetc  20906  frlmbasf  22046  frlmsplit2  22059  uvcff  22077  psrbag  22205  evlsval2  22376  evlsval3  22378  coe1fsupp  22512  gsummoncoe1  22606  evls1sca  22621  mamucl  22696  mamuvs1  22700  mamuvs2  22701  matbas2d  22718  matecl  22720  mamumat1cl  22734  mattposcl  22748  tposmap  22752  mat1dimelbas  22766  mavmulcl  22842  mdetunilem9  22915  matunitlindflem1  22974  matunitlindflem2  22975  matunitlindf  22976  pmatcollpw3lem  23081  pmatcollpw3fi1lem2  23085  cpmidpmatlem2  23169  cpmadumatpolylem1  23179  cayhamlem3  23185  cayhamlem4  23186  iscn  23533  iscnp  23535  cndis  23589  cnindis  23590  hausmapdom  23799  xkoptsub  23953  pt1hmeo  24105  flfval  24289  fcfval  24332  tmdgsum2  24395  symgtgp  24405  isucn  24576  ispsmet  24603  ismet  24622  isxmet  24623  imasdsf1olem  24672  elcncf  25190  metcld2  25608  elply2  26494  plyf  26496  elplyr  26499  plyeq0lem  26509  plyeq0  26510  plyaddlem  26514  plymullem  26515  dgrlem  26528  coeidlem  26536  ulmval  26689  ulmss  26706  ulmcn  26708  mtest  26713  pserulm  26731  isch2  31807  fmptco1f1o  33209  resf1o  33304  indf1ofs  33415  fedgmullem2  34244  smatrcl  34410  imambfm  34877  mbfmcnt  34883  isrrvv  35058  reprsuc  35227  reprinrn  35230  reprlt  35231  reprgt  35233  reprinfz1  35234  reprpmtf1o  35238  reprdifc  35239  circlevma  35254  deranglem  35900  indispconn  35968  prv1n  36165  knoppcnlem5  37333  knoppcnlem8  37336  fvopabf4g  38624  sdclem2  38644  sdclem1  38645  ismtyval  38702  rrncmslem  38734  aks6d1c2lem3  43144  aks6d1c5lem3  43155  aks6d1c5lem2  43156  sticksstones23  43187  mapfzcons  43680  mzpindd  43710  mzpsubst  43712  mzprename  43713  diophrw  43723  pw2f1ocnv  43997  ofoafg  44314  snelmap  46042  fvmap  46155  difmap  46163  mapssbi  46169  fourierdlem54  47114  fourierdlem111  47171  etransclem25  47213  qndenserrnbllem  47248  elhoi  47496  hoiprodcl2  47509  hoicvrrex  47510  ovnlecvr  47512  ovn0lem  47519  hsphoif  47530  hoidmvval  47531  hsphoival  47533  hoidmvle  47554  ovnhoilem1  47555  ovnhoilem2  47556  ovnlecvr2  47564  ovncvr2  47565  hoidifhspval2  47569  hoiqssbllem3  47578  hspmbllem2  47581  opnvonmbllem1  47586  nnsum3primesgbe  48834  nnsum4primesodd  48838  nnsum4primesoddALTV  48839  nnsum4primeseven  48842  nnsum4primesevenALTV  48843  isclintop  49248  funcringcsetcALTV2lem8  49338  funcringcsetclem8ALTV  49361  ofaddmndmap  49399  mapsnop  49400  zlmodzxzel  49411  linccl  49470  lincvalsc0  49477  lcoc0  49478  linc0scn0  49479  lincdifsn  49480  linc1  49481  lincsum  49485  lincscm  49486  lincscmcl  49488  lcoss  49492  lincext1  49510  lindslinindimp2lem2  49515  lindsrng01  49524  snlindsntorlem  49526  lincresunit1  49533  lincresunit3  49537  zlmodzxzldeplem1  49556  naryfvalel  49686  1arympt1fv  49695  1arymaptfo  49699  2arymaptf  49708  prelrrx2  49769  line2x  49810  line2y  49811  map0cor  49909