Theorem elmapg 8853

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  {cab 2713  Vcvv 3459  ⟶wf 6527  (class class class)co 7405   ↑_m cmap 8840

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-fv 6539  df-ov 7408  df-oprab 7409  df-mpo 7410  df-map 8842

This theorem is referenced by:  elmapd  8854  mapdm0  8856  elmapi  8863  elmap  8885  map0g  8898  fdiagfn  8904  ralxpmap  8910  ixpssmap2g  8941  snmapen  9052  pw2f1olem  9090  mapxpen  9157  fseqenlem1  10038  fseqdom  10040  infpwfien  10076  fin23lem17  10352  fin23lem39  10364  isf34lem6  10394  gruurn  10812  intgru  10828  grutsk1  10835  wrdval  14534  wrdnval  14563  vdwlem4  17004  vdwlem9  17009  vdwlem10  17010  vdwlem11  17011  vdwlem13  17013  vdw  17014  vdwnnlem1  17015  rami  17035  ramcl  17049  prmgaplcm  17080  pwselbasb  17502  funcestrcsetclem7  18158  funcestrcsetclem8  18159  fullestrcsetc  18163  funcsetcestrclem8  18174  funcsetcestrclem9  18175  fullsetcestrc  18178  mndvcl  18775  gsummptnn0fz  19967  isrnghm  20401  rnghmsscmap2  20589  rnghmsscmap  20590  funcrngcsetc  20600  funcrngcsetcALT  20601  rhmsscmap2  20618  rhmsscmap  20619  funcringcsetc  20634  frlmbasf  21720  frlmsplit2  21733  uvcff  21751  psrbag  21877  evlsval2  22045  coe1fsupp  22150  gsummoncoe1  22246  evls1sca  22261  mamucl  22339  mamuvs1  22343  mamuvs2  22344  matbas2d  22361  matecl  22363  mamumat1cl  22377  mattposcl  22391  tposmap  22395  mat1dimelbas  22409  mavmulcl  22485  mdetunilem9  22558  pmatcollpw3lem  22721  pmatcollpw3fi1lem2  22725  cpmidpmatlem2  22809  cpmadumatpolylem1  22819  cayhamlem3  22825  cayhamlem4  22826  iscn  23173  iscnp  23175  cndis  23229  cnindis  23230  hausmapdom  23438  xkoptsub  23592  pt1hmeo  23744  flfval  23928  fcfval  23971  tmdgsum2  24034  symgtgp  24044  isucn  24216  ispsmet  24243  ismet  24262  isxmet  24263  imasdsf1olem  24312  elcncf  24833  metcld2  25259  elply2  26153  plyf  26155  elplyr  26158  plyeq0lem  26167  plyeq0  26168  plyaddlem  26172  plymullem  26173  dgrlem  26186  coeidlem  26194  ulmval  26341  ulmss  26358  ulmcn  26360  mtest  26365  pserulm  26383  isch2  31204  fmptco1f1o  32611  resf1o  32707  indf1ofs  32843  fedgmullem2  33670  smatrcl  33827  imambfm  34294  mbfmcnt  34300  isrrvv  34475  reprsuc  34647  reprinrn  34650  reprlt  34651  reprgt  34653  reprinfz1  34654  reprpmtf1o  34658  reprdifc  34659  circlevma  34674  deranglem  35188  indispconn  35256  prv1n  35453  knoppcnlem5  36515  knoppcnlem8  36518  curf  37622  matunitlindflem1  37640  matunitlindflem2  37641  matunitlindf  37642  fvopabf4g  37746  sdclem2  37766  sdclem1  37767  ismtyval  37824  rrncmslem  37856  aks6d1c2lem3  42139  aks6d1c5lem3  42150  aks6d1c5lem2  42151  sticksstones23  42182  evlsval3  42582  mapfzcons  42739  mzpindd  42769  mzpsubst  42771  mzprename  42772  diophrw  42782  pw2f1ocnv  43061  ofoafg  43378  snelmap  45106  fvmap  45222  difmap  45231  mapssbi  45237  fourierdlem54  46189  fourierdlem111  46246  etransclem25  46288  qndenserrnbllem  46323  elhoi  46571  hoiprodcl2  46584  hoicvrrex  46585  ovnlecvr  46587  ovn0lem  46594  hsphoif  46605  hoidmvval  46606  hsphoival  46608  hoidmvle  46629  ovnhoilem1  46630  ovnhoilem2  46631  ovnlecvr2  46639  ovncvr2  46640  hoidifhspval2  46644  hoiqssbllem3  46653  hspmbllem2  46656  opnvonmbllem1  46661  nnsum3primesgbe  47806  nnsum4primesodd  47810  nnsum4primesoddALTV  47811  nnsum4primeseven  47814  nnsum4primesevenALTV  47815  isclintop  48182  funcringcsetcALTV2lem8  48272  funcringcsetclem8ALTV  48295  ofaddmndmap  48318  mapsnop  48319  zlmodzxzel  48330  linccl  48390  lincvalsc0  48397  lcoc0  48398  linc0scn0  48399  lincdifsn  48400  linc1  48401  lincsum  48405  lincscm  48406  lincscmcl  48408  lcoss  48412  lincext1  48430  lindslinindimp2lem2  48435  lindsrng01  48444  snlindsntorlem  48446  lincresunit1  48453  lincresunit3  48457  zlmodzxzldeplem1  48476  naryfvalel  48610  1arympt1fv  48619  1arymaptfo  48623  2arymaptf  48632  prelrrx2  48693  line2x  48734  line2y  48735  map0cor  48833