Theorem elmapg 8833

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   ∈ wcel 2107  {cab 2710  Vcvv 3475  ⟶wf 6540  (class class class)co 7409   ↑_m cmap 8820

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-map 8822

This theorem is referenced by:  elmapd  8834  mapdm0  8836  elmapi  8843  elmap  8865  map0g  8878  fdiagfn  8884  ralxpmap  8890  ixpssmap2g  8921  snmapen  9038  pw2f1olem  9076  mapxpen  9143  fseqenlem1  10019  fseqdom  10021  infpwfien  10057  fin23lem17  10333  fin23lem39  10345  isf34lem6  10375  gruurn  10793  intgru  10809  grutsk1  10816  hashfacenOLD  14414  wrdval  14467  wrdnval  14495  vdwlem4  16917  vdwlem9  16922  vdwlem10  16923  vdwlem11  16924  vdwlem13  16926  vdw  16927  vdwnnlem1  16928  rami  16948  ramcl  16962  prmgaplcm  16993  pwselbasb  17434  funcestrcsetclem7  18098  funcestrcsetclem8  18099  fullestrcsetc  18103  funcsetcestrclem8  18114  funcsetcestrclem9  18115  fullsetcestrc  18118  gsummptnn0fz  19854  frlmbasf  21315  frlmsplit2  21328  uvcff  21346  psrbag  21470  evlsval2  21650  coe1fsupp  21738  gsummoncoe1  21828  evls1sca  21842  mndvcl  21893  mamucl  21901  mamuvs1  21905  mamuvs2  21906  matbas2d  21925  matecl  21927  mamumat1cl  21941  mattposcl  21955  tposmap  21959  mat1dimelbas  21973  mavmulcl  22049  mdetunilem9  22122  pmatcollpw3lem  22285  pmatcollpw3fi1lem2  22289  cpmidpmatlem2  22373  cpmadumatpolylem1  22383  cayhamlem3  22389  cayhamlem4  22390  iscn  22739  iscnp  22741  cndis  22795  cnindis  22796  hausmapdom  23004  xkoptsub  23158  pt1hmeo  23310  flfval  23494  fcfval  23537  tmdgsum2  23600  symgtgp  23610  isucn  23783  ispsmet  23810  ismet  23829  isxmet  23830  imasdsf1olem  23879  elcncf  24405  metcld2  24824  elply2  25710  plyf  25712  elplyr  25715  plyeq0lem  25724  plyeq0  25725  plyaddlem  25729  plymullem  25730  dgrlem  25743  coeidlem  25751  ulmval  25892  ulmss  25909  ulmcn  25911  mtest  25916  pserulm  25934  isch2  30507  fmptco1f1o  31888  resf1o  31986  ply1degltdimlem  32738  fedgmullem2  32746  smatrcl  32807  indf1ofs  33055  imambfm  33292  mbfmcnt  33298  isrrvv  33473  reprsuc  33658  reprinrn  33661  reprlt  33662  reprgt  33664  reprinfz1  33665  reprpmtf1o  33669  reprdifc  33670  circlevma  33685  deranglem  34188  indispconn  34256  prv1n  34453  knoppcnlem5  35421  knoppcnlem8  35424  curf  36514  matunitlindflem1  36532  matunitlindflem2  36533  matunitlindf  36534  fvopabf4g  36638  sdclem2  36658  sdclem1  36659  ismtyval  36716  rrncmslem  36748  evlsval3  41179  mapfzcons  41502  mzpindd  41532  mzpsubst  41534  mzprename  41535  diophrw  41545  pw2f1ocnv  41824  ofoafg  42152  snelmap  43819  fvmap  43945  difmap  43954  mapssbi  43960  fourierdlem54  44924  fourierdlem111  44981  etransclem25  45023  qndenserrnbllem  45058  elhoi  45306  hoiprodcl2  45319  hoicvrrex  45320  ovnlecvr  45322  ovn0lem  45329  hsphoif  45340  hoidmvval  45341  hsphoival  45343  hoidmvle  45364  ovnhoilem1  45365  ovnhoilem2  45366  ovnlecvr2  45374  ovncvr2  45375  hoidifhspval2  45379  hoiqssbllem3  45388  hspmbllem2  45391  opnvonmbllem1  45396  nnsum3primesgbe  46508  nnsum4primesodd  46512  nnsum4primesoddALTV  46513  nnsum4primeseven  46516  nnsum4primesevenALTV  46517  isclintop  46665  isrnghm  46738  rnghmsscmap2  46919  rnghmsscmap  46920  funcrngcsetc  46944  funcrngcsetcALT  46945  rhmsscmap2  46965  rhmsscmap  46966  funcringcsetc  46981  funcringcsetcALTV2lem8  46989  funcringcsetclem8ALTV  47012  ofaddmndmap  47067  mapsnop  47068  zlmodzxzel  47079  linccl  47143  lincvalsc0  47150  lcoc0  47151  linc0scn0  47152  lincdifsn  47153  linc1  47154  lincsum  47158  lincscm  47159  lincscmcl  47161  lcoss  47165  lincext1  47183  lindslinindimp2lem2  47188  lindsrng01  47197  snlindsntorlem  47199  lincresunit1  47206  lincresunit3  47210  zlmodzxzldeplem1  47229  naryfvalel  47364  1arympt1fv  47373  1arymaptfo  47377  2arymaptf  47386  prelrrx2  47447  line2x  47488  line2y  47489  map0cor  47569