Theorem elmapg 8758

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2110  {cab 2708  Vcvv 3434  ⟶wf 6473  (class class class)co 7341   ↑_m cmap 8745

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7663

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3394  df-v 3436  df-sbc 3740  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4282  df-if 4474  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-opab 5152  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-iota 6433  df-fun 6479  df-fn 6480  df-f 6481  df-fv 6485  df-ov 7344  df-oprab 7345  df-mpo 7346  df-map 8747

This theorem is referenced by:  elmapd  8759  mapdm0  8761  elmapi  8768  elmap  8790  map0g  8803  fdiagfn  8809  ralxpmap  8815  ixpssmap2g  8846  snmapen  8955  pw2f1olem  8989  mapxpen  9051  fseqenlem1  9907  fseqdom  9909  infpwfien  9945  fin23lem17  10221  fin23lem39  10233  isf34lem6  10263  gruurn  10681  intgru  10697  grutsk1  10704  wrdval  14415  wrdnval  14444  vdwlem4  16888  vdwlem9  16893  vdwlem10  16894  vdwlem11  16895  vdwlem13  16897  vdw  16898  vdwnnlem1  16899  rami  16919  ramcl  16933  prmgaplcm  16964  pwselbasb  17384  funcestrcsetclem7  18044  funcestrcsetclem8  18045  fullestrcsetc  18049  funcsetcestrclem8  18060  funcsetcestrclem9  18061  fullsetcestrc  18064  mndvcl  18697  gsummptnn0fz  19891  isrnghm  20352  rnghmsscmap2  20537  rnghmsscmap  20538  funcrngcsetc  20548  funcrngcsetcALT  20549  rhmsscmap2  20566  rhmsscmap  20567  funcringcsetc  20582  frlmbasf  21690  frlmsplit2  21703  uvcff  21721  psrbag  21847  evlsval2  22015  coe1fsupp  22120  gsummoncoe1  22216  evls1sca  22231  mamucl  22309  mamuvs1  22313  mamuvs2  22314  matbas2d  22331  matecl  22333  mamumat1cl  22347  mattposcl  22361  tposmap  22365  mat1dimelbas  22379  mavmulcl  22455  mdetunilem9  22528  pmatcollpw3lem  22691  pmatcollpw3fi1lem2  22695  cpmidpmatlem2  22779  cpmadumatpolylem1  22789  cayhamlem3  22795  cayhamlem4  22796  iscn  23143  iscnp  23145  cndis  23199  cnindis  23200  hausmapdom  23408  xkoptsub  23562  pt1hmeo  23714  flfval  23898  fcfval  23941  tmdgsum2  24004  symgtgp  24014  isucn  24185  ispsmet  24212  ismet  24231  isxmet  24232  imasdsf1olem  24281  elcncf  24802  metcld2  25227  elply2  26121  plyf  26123  elplyr  26126  plyeq0lem  26135  plyeq0  26136  plyaddlem  26140  plymullem  26141  dgrlem  26154  coeidlem  26162  ulmval  26309  ulmss  26326  ulmcn  26328  mtest  26333  pserulm  26351  isch2  31193  fmptco1f1o  32605  resf1o  32703  indf1ofs  32837  fedgmullem2  33633  smatrcl  33799  imambfm  34265  mbfmcnt  34271  isrrvv  34446  reprsuc  34618  reprinrn  34621  reprlt  34622  reprgt  34624  reprinfz1  34625  reprpmtf1o  34629  reprdifc  34630  circlevma  34645  deranglem  35178  indispconn  35246  prv1n  35443  knoppcnlem5  36510  knoppcnlem8  36513  curf  37617  matunitlindflem1  37635  matunitlindflem2  37636  matunitlindf  37637  fvopabf4g  37741  sdclem2  37761  sdclem1  37762  ismtyval  37819  rrncmslem  37851  aks6d1c2lem3  42138  aks6d1c5lem3  42149  aks6d1c5lem2  42150  sticksstones23  42181  evlsval3  42571  mapfzcons  42728  mzpindd  42758  mzpsubst  42760  mzprename  42761  diophrw  42771  pw2f1ocnv  43049  ofoafg  43366  snelmap  45098  fvmap  45214  difmap  45223  mapssbi  45229  fourierdlem54  46177  fourierdlem111  46234  etransclem25  46276  qndenserrnbllem  46311  elhoi  46559  hoiprodcl2  46572  hoicvrrex  46573  ovnlecvr  46575  ovn0lem  46582  hsphoif  46593  hoidmvval  46594  hsphoival  46596  hoidmvle  46617  ovnhoilem1  46618  ovnhoilem2  46619  ovnlecvr2  46627  ovncvr2  46628  hoidifhspval2  46632  hoiqssbllem3  46641  hspmbllem2  46644  opnvonmbllem1  46649  nnsum3primesgbe  47802  nnsum4primesodd  47806  nnsum4primesoddALTV  47807  nnsum4primeseven  47810  nnsum4primesevenALTV  47811  isclintop  48217  funcringcsetcALTV2lem8  48307  funcringcsetclem8ALTV  48330  ofaddmndmap  48353  mapsnop  48354  zlmodzxzel  48365  linccl  48425  lincvalsc0  48432  lcoc0  48433  linc0scn0  48434  lincdifsn  48435  linc1  48436  lincsum  48440  lincscm  48441  lincscmcl  48443  lcoss  48447  lincext1  48465  lindslinindimp2lem2  48470  lindsrng01  48479  snlindsntorlem  48481  lincresunit1  48488  lincresunit3  48492  zlmodzxzldeplem1  48511  naryfvalel  48641  1arympt1fv  48650  1arymaptfo  48654  2arymaptf  48663  prelrrx2  48724  line2x  48765  line2y  48766  map0cor  48865