Theorem elmapg 8779

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  {cab 2715  Vcvv 3430  ⟶wf 6488  (class class class)co 7360   ↑_m cmap 8766

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-pow 5302  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7363  df-oprab 7364  df-mpo 7365  df-map 8768

This theorem is referenced by:  elmapd  8780  mapdm0  8782  elmapi  8789  elmap  8812  map0g  8825  fdiagfn  8831  ralxpmap  8837  ixpssmap2g  8868  snmapen  8978  pw2f1olem  9012  mapxpen  9074  fseqenlem1  9937  fseqdom  9939  infpwfien  9975  fin23lem17  10251  fin23lem39  10263  isf34lem6  10293  gruurn  10712  intgru  10728  grutsk1  10735  wrdval  14469  wrdnval  14498  vdwlem4  16946  vdwlem9  16951  vdwlem10  16952  vdwlem11  16953  vdwlem13  16955  vdw  16956  vdwnnlem1  16957  rami  16977  ramcl  16991  prmgaplcm  17022  pwselbasb  17442  funcestrcsetclem7  18103  funcestrcsetclem8  18104  fullestrcsetc  18108  funcsetcestrclem8  18119  funcsetcestrclem9  18120  fullsetcestrc  18123  mndvcl  18756  gsummptnn0fz  19952  isrnghm  20412  rnghmsscmap2  20597  rnghmsscmap  20598  funcrngcsetc  20608  funcrngcsetcALT  20609  rhmsscmap2  20626  rhmsscmap  20627  funcringcsetc  20642  frlmbasf  21750  frlmsplit2  21763  uvcff  21781  psrbag  21907  evlsval2  22075  evlsval3  22077  coe1fsupp  22188  gsummoncoe1  22283  evls1sca  22298  mamucl  22376  mamuvs1  22380  mamuvs2  22381  matbas2d  22398  matecl  22400  mamumat1cl  22414  mattposcl  22428  tposmap  22432  mat1dimelbas  22446  mavmulcl  22522  mdetunilem9  22595  pmatcollpw3lem  22758  pmatcollpw3fi1lem2  22762  cpmidpmatlem2  22846  cpmadumatpolylem1  22856  cayhamlem3  22862  cayhamlem4  22863  iscn  23210  iscnp  23212  cndis  23266  cnindis  23267  hausmapdom  23475  xkoptsub  23629  pt1hmeo  23781  flfval  23965  fcfval  24008  tmdgsum2  24071  symgtgp  24081  isucn  24252  ispsmet  24279  ismet  24298  isxmet  24299  imasdsf1olem  24348  elcncf  24866  metcld2  25284  elply2  26171  plyf  26173  elplyr  26176  plyeq0lem  26185  plyeq0  26186  plyaddlem  26190  plymullem  26191  dgrlem  26204  coeidlem  26212  ulmval  26358  ulmss  26375  ulmcn  26377  mtest  26382  pserulm  26400  isch2  31309  fmptco1f1o  32721  resf1o  32818  indf1ofs  32941  fedgmullem2  33790  smatrcl  33956  imambfm  34422  mbfmcnt  34428  isrrvv  34603  reprsuc  34775  reprinrn  34778  reprlt  34779  reprgt  34781  reprinfz1  34782  reprpmtf1o  34786  reprdifc  34787  circlevma  34802  deranglem  35364  indispconn  35432  prv1n  35629  knoppcnlem5  36773  knoppcnlem8  36776  curf  37933  matunitlindflem1  37951  matunitlindflem2  37952  matunitlindf  37953  fvopabf4g  38057  sdclem2  38077  sdclem1  38078  ismtyval  38135  rrncmslem  38167  aks6d1c2lem3  42579  aks6d1c5lem3  42590  aks6d1c5lem2  42591  sticksstones23  42622  mapfzcons  43162  mzpindd  43192  mzpsubst  43194  mzprename  43195  diophrw  43205  pw2f1ocnv  43483  ofoafg  43800  snelmap  45531  fvmap  45645  difmap  45654  mapssbi  45660  fourierdlem54  46606  fourierdlem111  46663  etransclem25  46705  qndenserrnbllem  46740  elhoi  46988  hoiprodcl2  47001  hoicvrrex  47002  ovnlecvr  47004  ovn0lem  47011  hsphoif  47022  hoidmvval  47023  hsphoival  47025  hoidmvle  47046  ovnhoilem1  47047  ovnhoilem2  47048  ovnlecvr2  47056  ovncvr2  47057  hoidifhspval2  47061  hoiqssbllem3  47070  hspmbllem2  47073  opnvonmbllem1  47078  nnsum3primesgbe  48280  nnsum4primesodd  48284  nnsum4primesoddALTV  48285  nnsum4primeseven  48288  nnsum4primesevenALTV  48289  isclintop  48695  funcringcsetcALTV2lem8  48785  funcringcsetclem8ALTV  48808  ofaddmndmap  48831  mapsnop  48832  zlmodzxzel  48843  linccl  48902  lincvalsc0  48909  lcoc0  48910  linc0scn0  48911  lincdifsn  48912  linc1  48913  lincsum  48917  lincscm  48918  lincscmcl  48920  lcoss  48924  lincext1  48942  lindslinindimp2lem2  48947  lindsrng01  48956  snlindsntorlem  48958  lincresunit1  48965  lincresunit3  48969  zlmodzxzldeplem1  48988  naryfvalel  49118  1arympt1fv  49127  1arymaptfo  49131  2arymaptf  49140  prelrrx2  49201  line2x  49242  line2y  49243  map0cor  49342