Theorem fnmpt 5714

Description: The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013.)

Hypothesis

Ref	Expression
mptfng.1	|- F = ( x e. A |-> B )

Assertion

Ref	Expression
fnmpt	|- ( A. x e. A B e. V -> F Fn A )

Distinct variable group:   x, A

Allowed substitution hints:   B( x)   F( x)   V( x)

Proof of Theorem fnmpt

Step	Hyp	Ref	Expression
1		elex 3040	. . 3 |- ( B e. V -> B e. _V )
2	1	ralimi 2796	. 2 |- ( A. x e. A B e. V -> A. x e. A B e. _V )
3		mptfng.1	. . 3 |- F = ( x e. A |-> B )
4	3	mptfng 5713	. 2 |- ( A. x e. A B e. _V <-> F Fn A )
5	2, 4	sylib 201	1 |- ( A. x e. A B e. V -> F Fn A )

Syntax hints:   -> wi 4   = wceq 1452   e. wcel 1904   A.wral 2756   _Vcvv 3031   |-> cmpt 4454   Fn wfn 5584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-fun 5591  df-fn 5592

This theorem is referenced by:  mpt0  5715  fnmptfvd  6000  ralrnmpt  6046  fmpt  6058  fmpt2d  6069  f1ocnvd  6537  offval2  6567  ofrfval2  6568  mptelixpg  7577  fifo  7964  cantnflem1  8212  infmap2  8666  compssiso  8822  gruiun  9242  mptnn0fsupp  12247  mptnn0fsuppr  12249  seqof  12308  rlimi2  13655  prdsbas3  15457  prdsbascl  15459  prdsdsval2  15460  quslem  15527  fnmrc  15591  isofn  15758  pmtrrn  17176  pmtrfrn  17177  pmtrdifwrdellem2  17201  gsummptcl  17677  dprdwdOLD  17722  mptscmfsupp0  18231  ofco2  19553  pmatcollpw2lem  19878  neif  20193  tgrest  20252  cmpfi  20500  elptr2  20666  xkoptsub  20746  ptcmplem2  21146  ptcmplem3  21147  prdsxmetlem  21461  prdsxmslem2  21622  bcth3  22377  uniioombllem6  22625  itg2const  22777  ellimc2  22911  dvrec  22988  dvmptres3  22989  ulmss  23431  ulmdvlem1  23434  ulmdvlem2  23435  ulmdvlem3  23436  itgulm2  23443  psercn  23460  f1o3d  28305  f1od2  28384  psgnfzto1stlem  28687  rmulccn  28808  esumnul  28943  esum0  28944  gsumesum  28954  ofcfval2  28999  signsplypnf  29511  signsply0  29512  cdlemk56  34609  dicfnN  34822  hbtlem7  36055  refsumcn  37414  wessf1ornlem  37530  choicefi  37552  fsumsermpt  37754  stoweidlem31  38004  stoweidlem59  38032  stirlinglem13  38060  dirkercncflem2  38078  fourierdlem62  38144  hoidmvlelem3  38537  dfafn5b  38808  lincresunit2  40779