Theorem elmapg 8812

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  {cab 2707  Vcvv 3447  ⟶wf 6507  (class class class)co 7387   ↑_m cmap 8799

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392  df-map 8801

This theorem is referenced by:  elmapd  8813  mapdm0  8815  elmapi  8822  elmap  8844  map0g  8857  fdiagfn  8863  ralxpmap  8869  ixpssmap2g  8900  snmapen  9009  pw2f1olem  9045  mapxpen  9107  fseqenlem1  9977  fseqdom  9979  infpwfien  10015  fin23lem17  10291  fin23lem39  10303  isf34lem6  10333  gruurn  10751  intgru  10767  grutsk1  10774  wrdval  14481  wrdnval  14510  vdwlem4  16955  vdwlem9  16960  vdwlem10  16961  vdwlem11  16962  vdwlem13  16964  vdw  16965  vdwnnlem1  16966  rami  16986  ramcl  17000  prmgaplcm  17031  pwselbasb  17451  funcestrcsetclem7  18107  funcestrcsetclem8  18108  fullestrcsetc  18112  funcsetcestrclem8  18123  funcsetcestrclem9  18124  fullsetcestrc  18127  mndvcl  18724  gsummptnn0fz  19916  isrnghm  20350  rnghmsscmap2  20538  rnghmsscmap  20539  funcrngcsetc  20549  funcrngcsetcALT  20550  rhmsscmap2  20567  rhmsscmap  20568  funcringcsetc  20583  frlmbasf  21669  frlmsplit2  21682  uvcff  21700  psrbag  21826  evlsval2  21994  coe1fsupp  22099  gsummoncoe1  22195  evls1sca  22210  mamucl  22288  mamuvs1  22292  mamuvs2  22293  matbas2d  22310  matecl  22312  mamumat1cl  22326  mattposcl  22340  tposmap  22344  mat1dimelbas  22358  mavmulcl  22434  mdetunilem9  22507  pmatcollpw3lem  22670  pmatcollpw3fi1lem2  22674  cpmidpmatlem2  22758  cpmadumatpolylem1  22768  cayhamlem3  22774  cayhamlem4  22775  iscn  23122  iscnp  23124  cndis  23178  cnindis  23179  hausmapdom  23387  xkoptsub  23541  pt1hmeo  23693  flfval  23877  fcfval  23920  tmdgsum2  23983  symgtgp  23993  isucn  24165  ispsmet  24192  ismet  24211  isxmet  24212  imasdsf1olem  24261  elcncf  24782  metcld2  25207  elply2  26101  plyf  26103  elplyr  26106  plyeq0lem  26115  plyeq0  26116  plyaddlem  26120  plymullem  26121  dgrlem  26134  coeidlem  26142  ulmval  26289  ulmss  26306  ulmcn  26308  mtest  26313  pserulm  26331  isch2  31152  fmptco1f1o  32557  resf1o  32653  indf1ofs  32789  fedgmullem2  33626  smatrcl  33786  imambfm  34253  mbfmcnt  34259  isrrvv  34434  reprsuc  34606  reprinrn  34609  reprlt  34610  reprgt  34612  reprinfz1  34613  reprpmtf1o  34617  reprdifc  34618  circlevma  34633  deranglem  35153  indispconn  35221  prv1n  35418  knoppcnlem5  36485  knoppcnlem8  36488  curf  37592  matunitlindflem1  37610  matunitlindflem2  37611  matunitlindf  37612  fvopabf4g  37716  sdclem2  37736  sdclem1  37737  ismtyval  37794  rrncmslem  37826  aks6d1c2lem3  42114  aks6d1c5lem3  42125  aks6d1c5lem2  42126  sticksstones23  42157  evlsval3  42547  mapfzcons  42704  mzpindd  42734  mzpsubst  42736  mzprename  42737  diophrw  42747  pw2f1ocnv  43026  ofoafg  43343  snelmap  45076  fvmap  45192  difmap  45201  mapssbi  45207  fourierdlem54  46158  fourierdlem111  46215  etransclem25  46257  qndenserrnbllem  46292  elhoi  46540  hoiprodcl2  46553  hoicvrrex  46554  ovnlecvr  46556  ovn0lem  46563  hsphoif  46574  hoidmvval  46575  hsphoival  46577  hoidmvle  46598  ovnhoilem1  46599  ovnhoilem2  46600  ovnlecvr2  46608  ovncvr2  46609  hoidifhspval2  46613  hoiqssbllem3  46622  hspmbllem2  46625  opnvonmbllem1  46630  nnsum3primesgbe  47793  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  isclintop  48195  funcringcsetcALTV2lem8  48285  funcringcsetclem8ALTV  48308  ofaddmndmap  48331  mapsnop  48332  zlmodzxzel  48343  linccl  48403  lincvalsc0  48410  lcoc0  48411  linc0scn0  48412  lincdifsn  48413  linc1  48414  lincsum  48418  lincscm  48419  lincscmcl  48421  lcoss  48425  lincext1  48443  lindslinindimp2lem2  48448  lindsrng01  48457  snlindsntorlem  48459  lincresunit1  48466  lincresunit3  48470  zlmodzxzldeplem1  48489  naryfvalel  48619  1arympt1fv  48628  1arymaptfo  48632  2arymaptf  48641  prelrrx2  48702  line2x  48743  line2y  48744  map0cor  48843