Theorem elmapg 8816

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 8813	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ↑m 𝐵) = {𝑔 ∣ 𝑔:𝐵⟶𝐴})
2	1	eleq2d 2847	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴}))
3		fex2 7913	. . . . 5 ⊢ ((𝐶:𝐵⟶𝐴 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 𝐶 ∈ V)
4	3	3com13 1136	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶:𝐵⟶𝐴) → 𝐶 ∈ V)
5	4	3expia 1133	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶:𝐵⟶𝐴 → 𝐶 ∈ V))
6		feq1 6665	. . . 4 ⊢ (𝑔 = 𝐶 → (𝑔:𝐵⟶𝐴 ↔ 𝐶:𝐵⟶𝐴))
7	6	elab3g 3644	. . 3 ⊢ ((𝐶:𝐵⟶𝐴 → 𝐶 ∈ V) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
8	5, 7	syl 17	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
9	2, 8	bitrd 281	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∈ wcel 2141  {cab 2739  Vcvv 3453  ⟶wf 6513  (class class class)co 7392   ↑_m cmap 8803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-pow 5321  ax-pr 5389  ax-un 7714

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3745  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-fv 6525  df-ov 7395  df-oprab 7396  df-mpo 7397  df-map 8805

This theorem is referenced by:  elmapd  8817  mapdm0  8819  elmapi  8826  elmap  8849  map0g  8862  fdiagfn  8868  ralxpmap  8874  ixpssmap2g  8905  snmapen  9015  pw2f1olem  9049  mapxpen  9111  fseqenlem1  9977  fseqdom  9979  infpwfien  10015  fin23lem17  10292  fin23lem39  10304  isf34lem6  10334  gruurn  10753  intgru  10769  grutsk1  10776  wrdval  14526  wrdnval  14555  vdwlem4  17003  vdwlem9  17008  vdwlem10  17009  vdwlem11  17010  vdwlem13  17012  vdw  17013  vdwnnlem1  17014  rami  17034  ramcl  17048  prmgaplcm  17079  pwselbasb  17500  funcestrcsetclem7  18161  funcestrcsetclem8  18162  fullestrcsetc  18166  funcsetcestrclem8  18177  funcsetcestrclem9  18178  fullsetcestrc  18181  mndvcl  18814  gsummptnn0fz  20009  isrnghm  20469  rnghmsscmap2  20658  rnghmsscmap  20659  funcrngcsetc  20669  funcrngcsetcALT  20670  rhmsscmap2  20687  rhmsscmap  20688  funcringcsetc  20703  frlmbasf  21792  frlmsplit2  21805  uvcff  21823  psrbag  21949  evlsval2  22120  evlsval3  22122  coe1fsupp  22256  gsummoncoe1  22351  evls1sca  22366  mamucl  22441  mamuvs1  22445  mamuvs2  22446  matbas2d  22463  matecl  22465  mamumat1cl  22479  mattposcl  22493  tposmap  22497  mat1dimelbas  22511  mavmulcl  22587  mdetunilem9  22660  pmatcollpw3lem  22823  pmatcollpw3fi1lem2  22827  cpmidpmatlem2  22911  cpmadumatpolylem1  22921  cayhamlem3  22927  cayhamlem4  22928  iscn  23275  iscnp  23277  cndis  23331  cnindis  23332  hausmapdom  23540  xkoptsub  23694  pt1hmeo  23846  flfval  24030  fcfval  24073  tmdgsum2  24136  symgtgp  24146  isucn  24317  ispsmet  24344  ismet  24363  isxmet  24364  imasdsf1olem  24413  elcncf  24931  metcld2  25349  elply2  26236  plyf  26238  elplyr  26241  plyeq0lem  26250  plyeq0  26251  plyaddlem  26255  plymullem  26256  dgrlem  26269  coeidlem  26277  ulmval  26420  ulmss  26437  ulmcn  26439  mtest  26444  pserulm  26462  isch2  31372  fmptco1f1o  32785  resf1o  32882  indf1ofs  33005  fedgmullem2  33888  smatrcl  34054  imambfm  34520  mbfmcnt  34526  isrrvv  34701  reprsuc  34873  reprinrn  34876  reprlt  34877  reprgt  34879  reprinfz1  34880  reprpmtf1o  34884  reprdifc  34885  circlevma  34900  deranglem  35480  indispconn  35548  prv1n  35745  knoppcnlem5  36899  knoppcnlem8  36902  curf  38061  matunitlindflem1  38079  matunitlindflem2  38080  matunitlindf  38081  fvopabf4g  38185  sdclem2  38205  sdclem1  38206  ismtyval  38263  rrncmslem  38295  aks6d1c2lem3  42707  aks6d1c5lem3  42718  aks6d1c5lem2  42719  sticksstones23  42750  mapfzcons  43261  mzpindd  43291  mzpsubst  43293  mzprename  43294  diophrw  43304  pw2f1ocnv  43578  ofoafg  43895  snelmap  45626  fvmap  45739  difmap  45747  mapssbi  45753  fourierdlem54  46698  fourierdlem111  46755  etransclem25  46797  qndenserrnbllem  46832  elhoi  47080  hoiprodcl2  47093  hoicvrrex  47094  ovnlecvr  47096  ovn0lem  47103  hsphoif  47114  hoidmvval  47115  hsphoival  47117  hoidmvle  47138  ovnhoilem1  47139  ovnhoilem2  47140  ovnlecvr2  47148  ovncvr2  47149  hoidifhspval2  47153  hoiqssbllem3  47162  hspmbllem2  47165  opnvonmbllem1  47170  nnsum3primesgbe  48378  nnsum4primesodd  48382  nnsum4primesoddALTV  48383  nnsum4primeseven  48386  nnsum4primesevenALTV  48387  isclintop  48793  funcringcsetcALTV2lem8  48883  funcringcsetclem8ALTV  48906  ofaddmndmap  48929  mapsnop  48930  zlmodzxzel  48941  linccl  49000  lincvalsc0  49007  lcoc0  49008  linc0scn0  49009  lincdifsn  49010  linc1  49011  lincsum  49015  lincscm  49016  lincscmcl  49018  lcoss  49022  lincext1  49040  lindslinindimp2lem2  49045  lindsrng01  49054  snlindsntorlem  49056  lincresunit1  49063  lincresunit3  49067  zlmodzxzldeplem1  49086  naryfvalel  49216  1arympt1fv  49225  1arymaptfo  49229  2arymaptf  49238  prelrrx2  49299  line2x  49340  line2y  49341  map0cor  49440