Theorem elmapg 7452

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

Assertion

Ref	Expression
elmapg

Proof of Theorem elmapg

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mapvalg 7449	. . 3
2	1	eleq2d 2527	. 2
3		fex2 6755	. . . . 5
4	3	3com13 1201	. . . 4
5	4	3expia 1198	. . 3
6		feq1 5718	. . . 4
7	6	elab3g 3252	. . 3
8	5, 7	syl 16	. 2
9	2, 8	bitrd 253	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  e.wcel 1818  {cab 2442  cvv 3109  -->wf 5589  (class class class)co 6296  cmap 7439

This theorem is referenced by:  elmapd  7453  elmapi  7460  elmap  7467  map0e  7476  map0g  7478  fdiagfn  7482  ralxpmap  7488  ixpssmap2g  7518  map1  7614  pw2f1olem  7641  mapxpen  7703  cantnfsOLD  8136  mapfienOLD  8159  fseqenlem1  8426  fseqdom  8428  infpwfien  8464  fin23lem17  8739  fin23lem39  8751  isf34lem6  8781  gruurn  9197  intgru  9213  grutsk1  9220  hashfacen  12503  wrdval  12551  wrdnval  12571  vdwlem4  14502  vdwlem9  14507  vdwlem10  14508  vdwlem11  14509  vdwlem13  14511  vdw  14512  vdwnnlem1  14513  rami  14533  ramcl  14547  pwselbasb  14885  symgbas  16405  gsummptnn0fz  17014  psrbag  18013  evlsval2  18189  coe1fsupp  18254  gsummoncoe1  18346  evls1sca  18360  frlmbasOLD  18787  frlmbasf  18794  frlmsplit2  18803  uvcff  18822  mndvcl  18893  mamucl  18903  mamuvs1  18907  mamuvs2  18908  matbas2d  18925  matecl  18927  mamumat1cl  18941  mattposcl  18955  tposmap  18959  mat1dimelbas  18973  mavmulcl  19049  mdetunilem9  19122  pmatcollpw3lem  19284  pmatcollpw3fi1lem2  19288  cpmidpmatlem2  19372  cpmadumatpolylem1  19382  cayhamlem3  19388  cayhamlem4  19389  iscn  19736  iscnp  19738  cndis  19792  cnindis  19793  hausmapdom  20001  xkoptsub  20155  pt1hmeo  20307  flfval  20491  fcfval  20534  tmdgsum2  20595  symgtgp  20600  isucn  20781  ispsmet  20808  ismet  20826  isxmet  20827  imasdsf1olem  20876  elcncf  21393  metcld2  21745  elply2  22593  plyf  22595  elplyr  22598  plyeq0lem  22607  plyeq0  22608  plyaddlem  22612  plymullem  22613  dgrlem  22626  coeidlem  22634  ulmval  22775  ulmss  22792  ulmcn  22794  mtest  22799  pserulm  22817  isch2  26141  resf1o  27553  indf1ofs  28039  imambfm  28233  mbfmcnt  28239  isrrvv  28382  deranglem  28610  indispcon  28679  fvopabf4g  30211  sdclem2  30235  sdclem1  30236  ismtyval  30296  rrncmslem  30328  mapfzcons  30648  mzpindd  30678  mzpsubst  30681  mzprename  30682  diophrw  30692  pw2f1ocnv  30979  fourierdlem54  31943  fourierdlem111  32000  etransclem25  32042  isclintop  32531  elestrchom  32634  estrcco  32636  funcestrcsetclem7  32652  funcestrcsetclem8  32653  fullestrcsetc  32657  funcsetcestrclem7  32667  funcsetcestrclem8  32668  funcsetcestrclem9  32669  fullsetcestrc  32672  isrnghm  32698  rnghmsscmap2  32781  rnghmsscmap  32782  funcrngcsetc  32806  funcrngcsetcALT  32807  rhmsscmap2  32827  rhmsscmap  32828  funcringcsetc  32843  funcringcsetcOLD2lem8  32851  funcringcsetclem8OLD  32874  ofaddmndmap  32933  mapsnop  32934  mapprop  32935  zlmodzxzel  32944  linccl  33015  lincvalsc0  33022  lcoc0  33023  linc0scn0  33024  lincdifsn  33025  linc1  33026  lincsum  33030  lincscm  33031  lincscmcl  33033  lcoss  33037  lincext1  33055  lindslinindimp2lem2  33060  lindsrng01  33069  snlindsntorlem  33071  lincresunit1  33078  lincresunit3  33082  zlmodzxzldeplem1  33101

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-fv 5601  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-map 7441