Theorem elmapg 8837

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 8834	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ↑m 𝐵) = {𝑔 ∣ 𝑔:𝐵⟶𝐴})
2	1	eleq2d 2849	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴}))
3		fex2 7934	. . . . 5 ⊢ ((𝐶:𝐵⟶𝐴 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 𝐶 ∈ V)
4	3	3com13 1142	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶:𝐵⟶𝐴) → 𝐶 ∈ V)
5	4	3expia 1139	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶:𝐵⟶𝐴 → 𝐶 ∈ V))
6		feq1 6685	. . . 4 ⊢ (𝑔 = 𝐶 → (𝑔:𝐵⟶𝐴 ↔ 𝐶:𝐵⟶𝐴))
7	6	elab3g 3645	. . 3 ⊢ ((𝐶:𝐵⟶𝐴 → 𝐶 ∈ V) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
8	5, 7	syl 18	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
9	2, 8	bitrd 282	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2143  {cab 2741  Vcvv 3455  ⟶wf 6534  (class class class)co 7412   ↑_m cmap 8825

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pow 5338  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546  df-ov 7415  df-oprab 7416  df-mpo 7417  df-map 8827

This theorem is referenced by:  elmapd  8838  mapdm0  8840  elmapi  8847  elmap  8870  map0g  8883  fdiagfn  8889  ralxpmap  8895  ixpssmap2g  8926  snmapen  9036  pw2f1olem  9070  mapxpen  9132  fseqenlem1  10009  fseqdom  10011  infpwfien  10047  fin23lem17  10323  fin23lem39  10335  isf34lem6  10365  gruurn  10784  intgru  10800  grutsk1  10807  wrdval  14555  wrdnval  14584  vdwlem4  17045  vdwlem9  17050  vdwlem10  17051  vdwlem11  17052  vdwlem13  17054  vdw  17055  vdwnnlem1  17056  rami  17076  ramcl  17090  prmgaplcm  17121  pwselbasb  17542  funcestrcsetclem7  18203  funcestrcsetclem8  18204  fullestrcsetc  18208  funcsetcestrclem8  18219  funcsetcestrclem9  18220  fullsetcestrc  18223  mndvcl  18856  gsummptnn0fz  20057  isrnghm  20524  rnghmsscmap2  20715  rnghmsscmap  20716  funcrngcsetc  20726  funcrngcsetcALT  20727  rhmsscmap2  20744  rhmsscmap  20745  funcringcsetc  20760  frlmbasf  21891  frlmsplit2  21904  uvcff  21922  psrbag  22048  evlsval2  22219  evlsval3  22221  coe1fsupp  22355  gsummoncoe1  22449  evls1sca  22464  mamucl  22539  mamuvs1  22543  mamuvs2  22544  matbas2d  22561  matecl  22563  mamumat1cl  22577  mattposcl  22591  tposmap  22595  mat1dimelbas  22609  mavmulcl  22685  mdetunilem9  22758  pmatcollpw3lem  22921  pmatcollpw3fi1lem2  22925  cpmidpmatlem2  23009  cpmadumatpolylem1  23019  cayhamlem3  23025  cayhamlem4  23026  iscn  23373  iscnp  23375  cndis  23429  cnindis  23430  hausmapdom  23638  xkoptsub  23792  pt1hmeo  23944  flfval  24128  fcfval  24171  tmdgsum2  24234  symgtgp  24244  isucn  24415  ispsmet  24442  ismet  24461  isxmet  24462  imasdsf1olem  24511  elcncf  25029  metcld2  25447  elply2  26334  plyf  26336  elplyr  26339  plyeq0lem  26348  plyeq0  26349  plyaddlem  26353  plymullem  26354  dgrlem  26367  coeidlem  26375  ulmval  26521  ulmss  26538  ulmcn  26540  mtest  26545  pserulm  26563  isch2  31553  fmptco1f1o  32956  resf1o  33053  indf1ofs  33164  fedgmullem2  33998  smatrcl  34164  imambfm  34630  mbfmcnt  34636  isrrvv  34811  reprsuc  34980  reprinrn  34983  reprlt  34984  reprgt  34986  reprinfz1  34987  reprpmtf1o  34991  reprdifc  34992  circlevma  35007  deranglem  35636  indispconn  35704  prv1n  35901  knoppcnlem5  37064  knoppcnlem8  37067  curf  38227  matunitlindflem1  38245  matunitlindflem2  38246  matunitlindf  38247  fvopabf4g  38351  sdclem2  38371  sdclem1  38372  ismtyval  38429  rrncmslem  38461  aks6d1c2lem3  42871  aks6d1c5lem3  42882  aks6d1c5lem2  42883  sticksstones23  42914  mapfzcons  43427  mzpindd  43457  mzpsubst  43459  mzprename  43460  diophrw  43470  pw2f1ocnv  43744  ofoafg  44061  snelmap  45782  fvmap  45895  difmap  45903  mapssbi  45909  fourierdlem54  46854  fourierdlem111  46911  etransclem25  46953  qndenserrnbllem  46988  elhoi  47236  hoiprodcl2  47249  hoicvrrex  47250  ovnlecvr  47252  ovn0lem  47259  hsphoif  47270  hoidmvval  47271  hsphoival  47273  hoidmvle  47294  ovnhoilem1  47295  ovnhoilem2  47296  ovnlecvr2  47304  ovncvr2  47305  hoidifhspval2  47309  hoiqssbllem3  47318  hspmbllem2  47321  opnvonmbllem1  47326  nnsum3primesgbe  48534  nnsum4primesodd  48538  nnsum4primesoddALTV  48539  nnsum4primeseven  48542  nnsum4primesevenALTV  48543  isclintop  48949  funcringcsetcALTV2lem8  49039  funcringcsetclem8ALTV  49062  ofaddmndmap  49100  mapsnop  49101  zlmodzxzel  49112  linccl  49171  lincvalsc0  49178  lcoc0  49179  linc0scn0  49180  lincdifsn  49181  linc1  49182  lincsum  49186  lincscm  49187  lincscmcl  49189  lcoss  49193  lincext1  49211  lindslinindimp2lem2  49216  lindsrng01  49225  snlindsntorlem  49227  lincresunit1  49234  lincresunit3  49238  zlmodzxzldeplem1  49257  naryfvalel  49387  1arympt1fv  49396  1arymaptfo  49400  2arymaptf  49409  prelrrx2  49470  line2x  49511  line2y  49512  map0cor  49610