Theorem elmapg 8833

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   ∈ wcel 2107  {cab 2710  Vcvv 3475  ⟶wf 6540  (class class class)co 7409   ↑_m cmap 8820

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-map 8822

This theorem is referenced by:  elmapd  8834  mapdm0  8836  elmapi  8843  elmap  8865  map0g  8878  fdiagfn  8884  ralxpmap  8890  ixpssmap2g  8921  snmapen  9038  pw2f1olem  9076  mapxpen  9143  fseqenlem1  10019  fseqdom  10021  infpwfien  10057  fin23lem17  10333  fin23lem39  10345  isf34lem6  10375  gruurn  10793  intgru  10809  grutsk1  10816  hashfacenOLD  14414  wrdval  14467  wrdnval  14495  vdwlem4  16917  vdwlem9  16922  vdwlem10  16923  vdwlem11  16924  vdwlem13  16926  vdw  16927  vdwnnlem1  16928  rami  16948  ramcl  16962  prmgaplcm  16993  pwselbasb  17434  funcestrcsetclem7  18098  funcestrcsetclem8  18099  fullestrcsetc  18103  funcsetcestrclem8  18114  funcsetcestrclem9  18115  fullsetcestrc  18118  gsummptnn0fz  19854  frlmbasf  21315  frlmsplit2  21328  uvcff  21346  psrbag  21470  evlsval2  21650  coe1fsupp  21738  gsummoncoe1  21828  evls1sca  21842  mndvcl  21893  mamucl  21901  mamuvs1  21905  mamuvs2  21906  matbas2d  21925  matecl  21927  mamumat1cl  21941  mattposcl  21955  tposmap  21959  mat1dimelbas  21973  mavmulcl  22049  mdetunilem9  22122  pmatcollpw3lem  22285  pmatcollpw3fi1lem2  22289  cpmidpmatlem2  22373  cpmadumatpolylem1  22383  cayhamlem3  22389  cayhamlem4  22390  iscn  22739  iscnp  22741  cndis  22795  cnindis  22796  hausmapdom  23004  xkoptsub  23158  pt1hmeo  23310  flfval  23494  fcfval  23537  tmdgsum2  23600  symgtgp  23610  isucn  23783  ispsmet  23810  ismet  23829  isxmet  23830  imasdsf1olem  23879  elcncf  24405  metcld2  24824  elply2  25710  plyf  25712  elplyr  25715  plyeq0lem  25724  plyeq0  25725  plyaddlem  25729  plymullem  25730  dgrlem  25743  coeidlem  25751  ulmval  25892  ulmss  25909  ulmcn  25911  mtest  25916  pserulm  25934  isch2  30476  fmptco1f1o  31857  resf1o  31955  ply1degltdimlem  32707  fedgmullem2  32715  smatrcl  32776  indf1ofs  33024  imambfm  33261  mbfmcnt  33267  isrrvv  33442  reprsuc  33627  reprinrn  33630  reprlt  33631  reprgt  33633  reprinfz1  33634  reprpmtf1o  33638  reprdifc  33639  circlevma  33654  deranglem  34157  indispconn  34225  prv1n  34422  knoppcnlem5  35373  knoppcnlem8  35376  curf  36466  matunitlindflem1  36484  matunitlindflem2  36485  matunitlindf  36486  fvopabf4g  36590  sdclem2  36610  sdclem1  36611  ismtyval  36668  rrncmslem  36700  evlsval3  41131  mapfzcons  41454  mzpindd  41484  mzpsubst  41486  mzprename  41487  diophrw  41497  pw2f1ocnv  41776  ofoafg  42104  snelmap  43771  fvmap  43897  difmap  43906  mapssbi  43912  fourierdlem54  44876  fourierdlem111  44933  etransclem25  44975  qndenserrnbllem  45010  elhoi  45258  hoiprodcl2  45271  hoicvrrex  45272  ovnlecvr  45274  ovn0lem  45281  hsphoif  45292  hoidmvval  45293  hsphoival  45295  hoidmvle  45316  ovnhoilem1  45317  ovnhoilem2  45318  ovnlecvr2  45326  ovncvr2  45327  hoidifhspval2  45331  hoiqssbllem3  45340  hspmbllem2  45343  opnvonmbllem1  45348  nnsum3primesgbe  46460  nnsum4primesodd  46464  nnsum4primesoddALTV  46465  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  isclintop  46617  isrnghm  46690  rnghmsscmap2  46871  rnghmsscmap  46872  funcrngcsetc  46896  funcrngcsetcALT  46897  rhmsscmap2  46917  rhmsscmap  46918  funcringcsetc  46933  funcringcsetcALTV2lem8  46941  funcringcsetclem8ALTV  46964  ofaddmndmap  47019  mapsnop  47020  zlmodzxzel  47031  linccl  47095  lincvalsc0  47102  lcoc0  47103  linc0scn0  47104  lincdifsn  47105  linc1  47106  lincsum  47110  lincscm  47111  lincscmcl  47113  lcoss  47117  lincext1  47135  lindslinindimp2lem2  47140  lindsrng01  47149  snlindsntorlem  47151  lincresunit1  47158  lincresunit3  47162  zlmodzxzldeplem1  47181  naryfvalel  47316  1arympt1fv  47325  1arymaptfo  47329  2arymaptf  47338  prelrrx2  47399  line2x  47440  line2y  47441  map0cor  47521