Theorem elmapg 7870

Description: Membership relation for set exponentiation. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 15-Nov-2014.)

Assertion

Ref	Expression
elmapg	|- ( ( A e. V /\ B e. W ) -> ( C e. ( A ^m B ) <-> C : B --> A ) )

Proof of Theorem elmapg

Dummy variable g is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mapvalg 7867	. . 3 |- ( ( A e. V /\ B e. W ) -> ( A ^m B ) = { g | g : B --> A } )
2	1	eleq2d 2687	. 2 |- ( ( A e. V /\ B e. W ) -> ( C e. ( A ^m B ) <-> C e. { g | g : B --> A } ) )
3		fex2 7121	. . . . 5 |- ( ( C : B --> A /\ B e. W /\ A e. V ) -> C e. _V )
4	3	3com13 1270	. . . 4 |- ( ( A e. V /\ B e. W /\ C : B --> A ) -> C e. _V )
5	4	3expia 1267	. . 3 |- ( ( A e. V /\ B e. W ) -> ( C : B --> A -> C e. _V ) )
6		feq1 6026	. . . 4 |- ( g = C -> ( g : B --> A <-> C : B --> A ) )
7	6	elab3g 3357	. . 3 |- ( ( C : B --> A -> C e. _V ) -> ( C e. { g | g : B --> A } <-> C : B --> A ) )
8	5, 7	syl 17	. 2 |- ( ( A e. V /\ B e. W ) -> ( C e. { g | g : B --> A } <-> C : B --> A ) )
9	2, 8	bitrd 268	1 |- ( ( A e. V /\ B e. W ) -> ( C e. ( A ^m B ) <-> C : B --> A ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   e. wcel 1990   {cab 2608   _Vcvv 3200   -->wf 5884  (class class class)co 6650   ^m cmap 7857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-map 7859

This theorem is referenced by:  elmapd  7871  mapdm0  7872  elmapi  7879  elmap  7886  map0e  7895  map0g  7897  fdiagfn  7901  ralxpmap  7907  ixpssmap2g  7937  map1  8036  pw2f1olem  8064  mapxpen  8126  fseqenlem1  8847  fseqdom  8849  infpwfien  8885  fin23lem17  9160  fin23lem39  9172  isf34lem6  9202  gruurn  9620  intgru  9636  grutsk1  9643  hashfacen  13238  wrdval  13308  wrdnval  13335  vdwlem4  15688  vdwlem9  15693  vdwlem10  15694  vdwlem11  15695  vdwlem13  15697  vdw  15698  vdwnnlem1  15699  rami  15719  ramcl  15733  prmgaplcm  15764  pwselbasb  16148  elestrchom  16768  estrcco  16770  funcestrcsetclem7  16786  funcestrcsetclem8  16787  fullestrcsetc  16791  funcsetcestrclem7  16801  funcsetcestrclem8  16802  funcsetcestrclem9  16803  fullsetcestrc  16806  symgbas  17800  gsummptnn0fz  18382  psrbag  19364  evlsval2  19520  coe1fsupp  19584  gsummoncoe1  19674  evls1sca  19688  frlmbasf  20104  frlmsplit2  20112  uvcff  20130  mndvcl  20197  mamucl  20207  mamuvs1  20211  mamuvs2  20212  matbas2d  20229  matecl  20231  mamumat1cl  20245  mattposcl  20259  tposmap  20263  mat1dimelbas  20277  mavmulcl  20353  mdetunilem9  20426  pmatcollpw3lem  20588  pmatcollpw3fi1lem2  20592  cpmidpmatlem2  20676  cpmadumatpolylem1  20686  cayhamlem3  20692  cayhamlem4  20693  iscn  21039  iscnp  21041  cndis  21095  cnindis  21096  hausmapdom  21303  xkoptsub  21457  pt1hmeo  21609  flfval  21794  fcfval  21837  tmdgsum2  21900  symgtgp  21905  isucn  22082  ispsmet  22109  ismet  22128  isxmet  22129  imasdsf1olem  22178  elcncf  22692  metcld2  23105  elply2  23952  plyf  23954  elplyr  23957  plyeq0lem  23966  plyeq0  23967  plyaddlem  23971  plymullem  23972  dgrlem  23985  coeidlem  23993  ulmval  24134  ulmss  24151  ulmcn  24153  mtest  24158  pserulm  24176  isch2  28080  fmptco1f1o  29434  resf1o  29505  smatrcl  29862  indf1ofs  30088  imambfm  30324  mbfmcnt  30330  isrrvv  30505  reprsuc  30693  reprinrn  30696  reprlt  30697  reprgt  30699  reprinfz1  30700  reprpmtf1o  30704  reprdifc  30705  circlevma  30720  deranglem  31148  indispconn  31216  knoppcnlem5  32487  knoppcnlem8  32490  curf  33387  matunitlindflem1  33405  matunitlindflem2  33406  matunitlindf  33407  fvopabf4g  33515  sdclem2  33538  sdclem1  33539  ismtyval  33599  rrncmslem  33631  mapfzcons  37279  mzpindd  37309  mzpsubst  37311  mzprename  37312  diophrw  37322  pw2f1ocnv  37604  snelmap  39254  mapdm0OLD  39383  fvmap  39387  mapsnd  39388  difmap  39399  mapssbi  39405  fourierdlem54  40377  fourierdlem111  40434  etransclem25  40476  qndenserrnbllem  40514  elhoi  40756  hoiprodcl2  40769  hoicvrrex  40770  ovnlecvr  40772  ovn0lem  40779  hsphoif  40790  hoidmvval  40791  hsphoival  40793  hoidmvle  40814  ovnhoilem1  40815  ovnhoilem2  40816  ovnlecvr2  40824  ovncvr2  40825  hoidifhspval2  40829  hoiqssbllem3  40838  hspmbllem2  40841  opnvonmbllem1  40846  nnsum3primesgbe  41680  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  isclintop  41843  isrnghm  41892  rnghmsscmap2  41973  rnghmsscmap  41974  funcrngcsetc  41998  funcrngcsetcALT  41999  rhmsscmap2  42019  rhmsscmap  42020  funcringcsetc  42035  funcringcsetcALTV2lem8  42043  funcringcsetclem8ALTV  42066  ofaddmndmap  42122  mapsnop  42123  mapprop  42124  zlmodzxzel  42133  linccl  42203  lincvalsc0  42210  lcoc0  42211  linc0scn0  42212  lincdifsn  42213  linc1  42214  lincsum  42218  lincscm  42219  lincscmcl  42221  lcoss  42225  lincext1  42243  lindslinindimp2lem2  42248  lindsrng01  42257  snlindsntorlem  42259  lincresunit1  42266  lincresunit3  42270  zlmodzxzldeplem1  42289