Theorem fnmpt 5640

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 3081	. . 3 |- ( B e. V -> B e. _V )
2	1	ralimi 2816	. 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 5639	. 2 |- ( A. x e. A B e. _V <-> F Fn A )
5	2, 4	sylib 196	1 |- ( A. x e. A B e. V -> F Fn A )

Syntax hints:   -> wi 4   = wceq 1370   e. wcel 1758   A.wral 2796   _Vcvv 3072   |-> cmpt 4453   Fn wfn 5516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954  ax-ext 2431  ax-sep 4516  ax-nul 4524  ax-pr 4634

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2265  df-mo 2266  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-ne 2647  df-ral 2801  df-rex 2802  df-rab 2805  df-v 3074  df-dif 3434  df-un 3436  df-in 3438  df-ss 3445  df-nul 3741  df-if 3895  df-sn 3981  df-pr 3983  df-op 3987  df-br 4396  df-opab 4454  df-mpt 4455  df-id 4739  df-xp 4949  df-rel 4950  df-cnv 4951  df-co 4952  df-dm 4953  df-fun 5523  df-fn 5524

This theorem is referenced by:  mpt0  5641  fnmptfvd  5910  ralrnmpt  5956  fmpt  5968  fmpt2d  5977  f1ocnvd  6414  offval2  6441  ofrfval2  6442  mptelixpg  7405  fifo  7788  cantnflem1  8003  infmap2  8493  compssiso  8649  gruiun  9072  seqof  11975  rlimi2  13105  rlimmptrcl  13198  prdsbas3  14533  prdsbascl  14535  prdsdsval2  14536  divslem  14595  fnmrc  14659  pmtrrn  16077  pmtrfrn  16078  pmtrdifwrdellem2  16102  gsummptcl  16575  dprdwd  16612  dprdwdOLD  16618  mptscmfsupp0  17129  ofco2  18454  neif  18831  tgrest  18890  cmpfi  19138  elptr2  19274  xkoptsub  19354  ptcmplem2  19752  ptcmplem3  19753  prdsxmetlem  20070  prdsxmslem2  20231  bcth3  20969  uniioombllem6  21196  itg2const  21346  iblcnlem  21394  ellimc2  21480  dvrec  21557  dvmptres3  21558  ulmss  21990  ulmdvlem1  21993  ulmdvlem2  21994  ulmdvlem3  21995  itgulm2  22002  psercn  22019  f1o3d  26094  f1od2  26170  rmulccn  26498  esumnul  26642  esum0  26643  ofcfval2  26686  signsplypnf  27090  signsply0  27091  signstlen  27107  hbtlem7  29624  refsumcn  29895  stoweidlem31  29969  stoweidlem59  29997  stirlinglem13  30024  dfafn5b  30210  mptnn0fsupp  30945  mptnn0fsuppr  30947  lincresunit2  31126  pmatcollpw2lem  31246  cdlemk56  34934  dicfnN  35147