Theorem elmapg 8783

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 8780	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ↑m 𝐵) = {𝑔 ∣ 𝑔:𝐵⟶𝐴})
2	1	eleq2d 2826	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴}))
3		fex2 7883	. . . . 5 ⊢ ((𝐶:𝐵⟶𝐴 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 𝐶 ∈ V)
4	3	3com13 1130	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶:𝐵⟶𝐴) → 𝐶 ∈ V)
5	4	3expia 1127	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶:𝐵⟶𝐴 → 𝐶 ∈ V))
6		feq1 6640	. . . 4 ⊢ (𝑔 = 𝐶 → (𝑔:𝐵⟶𝐴 ↔ 𝐶:𝐵⟶𝐴))
7	6	elab3g 3630	. . 3 ⊢ ((𝐶:𝐵⟶𝐴 → 𝐶 ∈ V) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
8	5, 7	syl 17	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
9	2, 8	bitrd 280	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∈ wcel 2119  {cab 2718  Vcvv 3432  ⟶wf 6488  (class class class)co 7363   ↑_m cmap 8770

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7366  df-oprab 7367  df-mpo 7368  df-map 8772

This theorem is referenced by:  elmapd  8784  mapdm0  8786  elmapi  8793  elmap  8816  map0g  8829  fdiagfn  8835  ralxpmap  8841  ixpssmap2g  8872  snmapen  8982  pw2f1olem  9016  mapxpen  9078  fseqenlem1  9944  fseqdom  9946  infpwfien  9982  fin23lem17  10258  fin23lem39  10270  isf34lem6  10300  gruurn  10719  intgru  10735  grutsk1  10742  wrdval  14476  wrdnval  14505  vdwlem4  16953  vdwlem9  16958  vdwlem10  16959  vdwlem11  16960  vdwlem13  16962  vdw  16963  vdwnnlem1  16964  rami  16984  ramcl  16998  prmgaplcm  17029  pwselbasb  17449  funcestrcsetclem7  18110  funcestrcsetclem8  18111  fullestrcsetc  18115  funcsetcestrclem8  18126  funcsetcestrclem9  18127  fullsetcestrc  18130  mndvcl  18763  gsummptnn0fz  19959  isrnghm  20419  rnghmsscmap2  20608  rnghmsscmap  20609  funcrngcsetc  20619  funcrngcsetcALT  20620  rhmsscmap2  20637  rhmsscmap  20638  funcringcsetc  20653  frlmbasf  21742  frlmsplit2  21755  uvcff  21773  psrbag  21899  evlsval2  22070  evlsval3  22072  coe1fsupp  22206  gsummoncoe1  22301  evls1sca  22316  mamucl  22391  mamuvs1  22395  mamuvs2  22396  matbas2d  22413  matecl  22415  mamumat1cl  22429  mattposcl  22443  tposmap  22447  mat1dimelbas  22461  mavmulcl  22537  mdetunilem9  22610  pmatcollpw3lem  22773  pmatcollpw3fi1lem2  22777  cpmidpmatlem2  22861  cpmadumatpolylem1  22871  cayhamlem3  22877  cayhamlem4  22878  iscn  23225  iscnp  23227  cndis  23281  cnindis  23282  hausmapdom  23490  xkoptsub  23644  pt1hmeo  23796  flfval  23980  fcfval  24023  tmdgsum2  24086  symgtgp  24096  isucn  24267  ispsmet  24294  ismet  24313  isxmet  24314  imasdsf1olem  24363  elcncf  24881  metcld2  25299  elply2  26186  plyf  26188  elplyr  26191  plyeq0lem  26200  plyeq0  26201  plyaddlem  26205  plymullem  26206  dgrlem  26219  coeidlem  26227  ulmval  26370  ulmss  26387  ulmcn  26389  mtest  26394  pserulm  26412  isch2  31319  fmptco1f1o  32732  resf1o  32829  indf1ofs  32952  fedgmullem2  33821  smatrcl  33987  imambfm  34453  mbfmcnt  34459  isrrvv  34634  reprsuc  34806  reprinrn  34809  reprlt  34810  reprgt  34812  reprinfz1  34813  reprpmtf1o  34817  reprdifc  34818  circlevma  34833  deranglem  35401  indispconn  35469  prv1n  35666  knoppcnlem5  36810  knoppcnlem8  36813  curf  37972  matunitlindflem1  37990  matunitlindflem2  37991  matunitlindf  37992  fvopabf4g  38096  sdclem2  38116  sdclem1  38117  ismtyval  38174  rrncmslem  38206  aks6d1c2lem3  42618  aks6d1c5lem3  42629  aks6d1c5lem2  42630  sticksstones23  42661  mapfzcons  43172  mzpindd  43202  mzpsubst  43204  mzprename  43205  diophrw  43215  pw2f1ocnv  43489  ofoafg  43806  snelmap  45537  fvmap  45651  difmap  45659  mapssbi  45665  fourierdlem54  46610  fourierdlem111  46667  etransclem25  46709  qndenserrnbllem  46744  elhoi  46992  hoiprodcl2  47005  hoicvrrex  47006  ovnlecvr  47008  ovn0lem  47015  hsphoif  47026  hoidmvval  47027  hsphoival  47029  hoidmvle  47050  ovnhoilem1  47051  ovnhoilem2  47052  ovnlecvr2  47060  ovncvr2  47061  hoidifhspval2  47065  hoiqssbllem3  47074  hspmbllem2  47077  opnvonmbllem1  47082  nnsum3primesgbe  48290  nnsum4primesodd  48294  nnsum4primesoddALTV  48295  nnsum4primeseven  48298  nnsum4primesevenALTV  48299  isclintop  48705  funcringcsetcALTV2lem8  48795  funcringcsetclem8ALTV  48818  ofaddmndmap  48841  mapsnop  48842  zlmodzxzel  48853  linccl  48912  lincvalsc0  48919  lcoc0  48920  linc0scn0  48921  lincdifsn  48922  linc1  48923  lincsum  48927  lincscm  48928  lincscmcl  48930  lcoss  48934  lincext1  48952  lindslinindimp2lem2  48957  lindsrng01  48966  snlindsntorlem  48968  lincresunit1  48975  lincresunit3  48979  zlmodzxzldeplem1  48998  naryfvalel  49128  1arympt1fv  49137  1arymaptfo  49141  2arymaptf  49150  prelrrx2  49211  line2x  49252  line2y  49253  map0cor  49352