Theorem fnmpt 5713

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 3118	. . 3 |- ( B e. V -> B e. _V )
2	1	ralimi 2850	. 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 5712	. 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 1395   e. wcel 1819   A.wral 2807   _Vcvv 3109   |-> cmpt 4515   Fn wfn 5589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pr 4695

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  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-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-br 4457  df-opab 4516  df-mpt 4517  df-id 4804  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-fun 5596  df-fn 5597

This theorem is referenced by:  mpt0  5714  fnmptfvd  5991  ralrnmpt  6041  fmpt  6053  fmpt2d  6062  f1ocnvd  6523  offval2  6555  ofrfval2  6556  mptelixpg  7525  fifo  7910  cantnflem1  8125  infmap2  8615  compssiso  8771  gruiun  9194  mptnn0fsupp  12105  mptnn0fsuppr  12107  seqof  12166  rlimi2  13348  prdsbas3  14897  prdsbascl  14899  prdsdsval2  14900  quslem  14959  fnmrc  15023  isofn  15190  pmtrrn  16608  pmtrfrn  16609  pmtrdifwrdellem2  16633  gsummptcl  17120  dprdwdOLD2  17171  dprdwdOLD  17177  mptscmfsupp0  17702  ofco2  19079  pmatcollpw2lem  19404  neif  19727  tgrest  19786  cmpfi  20034  elptr2  20200  xkoptsub  20280  ptcmplem2  20678  ptcmplem3  20679  prdsxmetlem  20996  prdsxmslem2  21157  bcth3  21895  uniioombllem6  22122  itg2const  22272  ellimc2  22406  dvrec  22483  dvmptres3  22484  ulmss  22917  ulmdvlem1  22920  ulmdvlem2  22921  ulmdvlem3  22922  itgulm2  22929  psercn  22946  f1o3d  27613  f1od2  27697  rmulccn  28063  esumnul  28214  esum0  28215  gsumesum  28222  ofcfval2  28264  signsplypnf  28682  signsply0  28683  hbtlem7  31236  refsumcn  31566  stoweidlem31  31974  stoweidlem59  32002  stirlinglem13  32029  dirkercncflem2  32047  fourierdlem62  32112  dfafn5b  32407  lincresunit2  33181  cdlemk56  36798  dicfnN  37011