Theorem elmapg 8413

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 8410	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ↑m 𝐵) = {𝑔 ∣ 𝑔:𝐵⟶𝐴})
2	1	eleq2d 2898	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴}))
3		fex2 7632	. . . . 5 ⊢ ((𝐶:𝐵⟶𝐴 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 𝐶 ∈ V)
4	3	3com13 1120	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶:𝐵⟶𝐴) → 𝐶 ∈ V)
5	4	3expia 1117	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶:𝐵⟶𝐴 → 𝐶 ∈ V))
6		feq1 6490	. . . 4 ⊢ (𝑔 = 𝐶 → (𝑔:𝐵⟶𝐴 ↔ 𝐶:𝐵⟶𝐴))
7	6	elab3g 3673	. . 3 ⊢ ((𝐶:𝐵⟶𝐴 → 𝐶 ∈ V) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
8	5, 7	syl 17	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
9	2, 8	bitrd 281	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∈ wcel 2110  {cab 2799  Vcvv 3495  ⟶wf 6346  (class class class)co 7150   ↑_m cmap 8400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-br 5060  df-opab 5122  df-id 5455  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-fv 6358  df-ov 7153  df-oprab 7154  df-mpo 7155  df-map 8402

This theorem is referenced by:  elmapd  8414  mapdm0  8415  elmapi  8422  elmap  8429  map0g  8442  fdiagfn  8448  ralxpmap  8454  ixpssmap2g  8485  snmapen  8584  pw2f1olem  8615  mapxpen  8677  fseqenlem1  9444  fseqdom  9446  infpwfien  9482  fin23lem17  9754  fin23lem39  9766  isf34lem6  9796  gruurn  10214  intgru  10230  grutsk1  10237  hashfacen  13806  wrdval  13858  wrdnval  13890  vdwlem4  16314  vdwlem9  16319  vdwlem10  16320  vdwlem11  16321  vdwlem13  16323  vdw  16324  vdwnnlem1  16325  rami  16345  ramcl  16359  prmgaplcm  16390  pwselbasb  16755  funcestrcsetclem7  17390  funcestrcsetclem8  17391  fullestrcsetc  17395  funcsetcestrclem8  17406  funcsetcestrclem9  17407  fullsetcestrc  17410  gsummptnn0fz  19100  psrbag  20138  evlsval2  20294  coe1fsupp  20376  gsummoncoe1  20466  evls1sca  20480  frlmbasf  20898  frlmsplit2  20911  uvcff  20929  mndvcl  20996  mamucl  21004  mamuvs1  21008  mamuvs2  21009  matbas2d  21026  matecl  21028  mamumat1cl  21042  mattposcl  21056  tposmap  21060  mat1dimelbas  21074  mavmulcl  21150  mdetunilem9  21223  pmatcollpw3lem  21385  pmatcollpw3fi1lem2  21389  cpmidpmatlem2  21473  cpmadumatpolylem1  21483  cayhamlem3  21489  cayhamlem4  21490  iscn  21837  iscnp  21839  cndis  21893  cnindis  21894  hausmapdom  22102  xkoptsub  22256  pt1hmeo  22408  flfval  22592  fcfval  22635  tmdgsum2  22698  symgtgp  22708  isucn  22881  ispsmet  22908  ismet  22927  isxmet  22928  imasdsf1olem  22977  elcncf  23491  metcld2  23904  elply2  24780  plyf  24782  elplyr  24785  plyeq0lem  24794  plyeq0  24795  plyaddlem  24799  plymullem  24800  dgrlem  24813  coeidlem  24821  ulmval  24962  ulmss  24979  ulmcn  24981  mtest  24986  pserulm  25004  isch2  28994  fmptco1f1o  30372  resf1o  30460  fedgmullem2  31021  smatrcl  31056  indf1ofs  31280  imambfm  31515  mbfmcnt  31521  isrrvv  31696  reprsuc  31881  reprinrn  31884  reprlt  31885  reprgt  31887  reprinfz1  31888  reprpmtf1o  31892  reprdifc  31893  circlevma  31908  deranglem  32408  indispconn  32476  prv1n  32673  knoppcnlem5  33831  knoppcnlem8  33834  curf  34864  matunitlindflem1  34882  matunitlindflem2  34883  matunitlindf  34884  fvopabf4g  34990  sdclem2  35011  sdclem1  35012  ismtyval  35072  rrncmslem  35104  mapfzcons  39306  mzpindd  39336  mzpsubst  39338  mzprename  39339  diophrw  39349  pw2f1ocnv  39627  snelmap  41339  fvmap  41452  difmap  41462  mapssbi  41468  fourierdlem54  42438  fourierdlem111  42495  etransclem25  42537  qndenserrnbllem  42572  elhoi  42817  hoiprodcl2  42830  hoicvrrex  42831  ovnlecvr  42833  ovn0lem  42840  hsphoif  42851  hoidmvval  42852  hsphoival  42854  hoidmvle  42875  ovnhoilem1  42876  ovnhoilem2  42877  ovnlecvr2  42885  ovncvr2  42886  hoidifhspval2  42890  hoiqssbllem3  42899  hspmbllem2  42902  opnvonmbllem1  42907  nnsum3primesgbe  43950  nnsum4primesodd  43954  nnsum4primesoddALTV  43955  nnsum4primeseven  43958  nnsum4primesevenALTV  43959  isclintop  44107  isrnghm  44156  rnghmsscmap2  44237  rnghmsscmap  44238  funcrngcsetc  44262  funcrngcsetcALT  44263  rhmsscmap2  44283  rhmsscmap  44284  funcringcsetc  44299  funcringcsetcALTV2lem8  44307  funcringcsetclem8ALTV  44330  ofaddmndmap  44385  mapsnop  44386  mapprop  44387  zlmodzxzel  44396  linccl  44462  lincvalsc0  44469  lcoc0  44470  linc0scn0  44471  lincdifsn  44472  linc1  44473  lincsum  44477  lincscm  44478  lincscmcl  44480  lcoss  44484  lincext1  44502  lindslinindimp2lem2  44507  lindsrng01  44516  snlindsntorlem  44518  lincresunit1  44525  lincresunit3  44529  zlmodzxzldeplem1  44548  prelrrx2  44693  line2x  44734  line2y  44735