Theorem elmapg 8845

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2146  {cab 2744  Vcvv 3458  ⟶wf 6539  (class class class)co 7423   ↑_m cmap 8833

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-pow 5341  ax-pr 5409  ax-un 7745

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7426  df-oprab 7427  df-mpo 7428  df-map 8835

This theorem is used by:  elmapd  8846  mapdm0  8848  elmapi  8855  elmap  8878  map0g  8891  fdiagfn  8897  ralxpmap  8903  ixpssmap2g  8934  snmapen  9045  pw2f1olem  9079  mapxpen  9141  fseqenlem1  10027  fseqdom  10029  infpwfien  10065  fin23lem17  10340  fin23lem39  10352  isf34lem6  10382  gruurn  10801  intgru  10817  grutsk1  10824  wrdval  14573  wrdnval  14602  vdwlem4  17069  vdwlem9  17074  vdwlem10  17075  vdwlem11  17076  vdwlem13  17078  vdw  17079  vdwnnlem1  17080  rami  17100  ramcl  17114  prmgaplcm  17145  pwselbasb  17566  funcestrcsetclem7  18227  funcestrcsetclem8  18228  fullestrcsetc  18232  funcsetcestrclem8  18243  funcsetcestrclem9  18244  fullsetcestrc  18247  mndvcl  18886  gsummptnn0fz  20087  isrnghm  20556  rnghmsscmap2  20765  rnghmsscmap  20766  funcrngcsetc  20776  funcrngcsetcALT  20777  rhmsscmap2  20794  rhmsscmap  20795  funcringcsetc  20810  frlmbasf  21947  frlmsplit2  21960  uvcff  21978  psrbag  22104  evlsval2  22275  evlsval3  22277  coe1fsupp  22411  gsummoncoe1  22505  evls1sca  22520  mamucl  22595  mamuvs1  22599  mamuvs2  22600  matbas2d  22617  matecl  22619  mamumat1cl  22633  mattposcl  22647  tposmap  22651  mat1dimelbas  22665  mavmulcl  22741  mdetunilem9  22814  pmatcollpw3lem  22977  pmatcollpw3fi1lem2  22981  cpmidpmatlem2  23065  cpmadumatpolylem1  23075  cayhamlem3  23081  cayhamlem4  23082  iscn  23429  iscnp  23431  cndis  23485  cnindis  23486  hausmapdom  23694  xkoptsub  23848  pt1hmeo  24000  flfval  24184  fcfval  24227  tmdgsum2  24290  symgtgp  24300  isucn  24471  ispsmet  24498  ismet  24517  isxmet  24518  imasdsf1olem  24567  elcncf  25085  metcld2  25503  elply2  26390  plyf  26392  elplyr  26395  plyeq0lem  26404  plyeq0  26405  plyaddlem  26409  plymullem  26410  dgrlem  26423  coeidlem  26431  ulmval  26580  ulmss  26597  ulmcn  26599  mtest  26604  pserulm  26622  isch2  31612  fmptco1f1o  33015  resf1o  33112  indf1ofs  33223  fedgmullem2  34051  smatrcl  34217  imambfm  34684  mbfmcnt  34690  isrrvv  34865  reprsuc  35034  reprinrn  35037  reprlt  35038  reprgt  35040  reprinfz1  35041  reprpmtf1o  35045  reprdifc  35046  circlevma  35061  deranglem  35679  indispconn  35747  prv1n  35944  knoppcnlem5  37127  knoppcnlem8  37130  curf  38290  matunitlindflem1  38308  matunitlindflem2  38309  matunitlindf  38310  fvopabf4g  38414  sdclem2  38434  sdclem1  38435  ismtyval  38492  rrncmslem  38524  aks6d1c2lem3  42934  aks6d1c5lem3  42945  aks6d1c5lem2  42946  sticksstones23  42977  mapfzcons  43488  mzpindd  43518  mzpsubst  43520  mzprename  43521  diophrw  43531  pw2f1ocnv  43805  ofoafg  44122  snelmap  45843  fvmap  45956  difmap  45964  mapssbi  45970  fourierdlem54  46915  fourierdlem111  46972  etransclem25  47014  qndenserrnbllem  47049  elhoi  47297  hoiprodcl2  47310  hoicvrrex  47311  ovnlecvr  47313  ovn0lem  47320  hsphoif  47331  hoidmvval  47332  hsphoival  47334  hoidmvle  47355  ovnhoilem1  47356  ovnhoilem2  47357  ovnlecvr2  47365  ovncvr2  47366  hoidifhspval2  47370  hoiqssbllem3  47379  hspmbllem2  47382  opnvonmbllem1  47387  nnsum3primesgbe  48598  nnsum4primesodd  48602  nnsum4primesoddALTV  48603  nnsum4primeseven  48606  nnsum4primesevenALTV  48607  isclintop  49013  funcringcsetcALTV2lem8  49103  funcringcsetclem8ALTV  49126  ofaddmndmap  49164  mapsnop  49165  zlmodzxzel  49176  linccl  49235  lincvalsc0  49242  lcoc0  49243  linc0scn0  49244  lincdifsn  49245  linc1  49246  lincsum  49250  lincscm  49251  lincscmcl  49253  lcoss  49257  lincext1  49275  lindslinindimp2lem2  49280  lindsrng01  49289  snlindsntorlem  49291  lincresunit1  49298  lincresunit3  49302  zlmodzxzldeplem1  49321  naryfvalel  49451  1arympt1fv  49460  1arymaptfo  49464  2arymaptf  49473  prelrrx2  49534  line2x  49575  line2y  49576  map0cor  49674