Theorem fnmpt 5722

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 3089	. . 3 |- ( B e. V -> B e. _V )
2	1	ralimi 2815	. 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 5721	. 2 |- ( A. x e. A B e. _V <-> F Fn A )
5	2, 4	sylib 199	1 |- ( A. x e. A B e. V -> F Fn A )

Syntax hints:   -> wi 4   = wceq 1437   e. wcel 1872   A.wral 2771   _Vcvv 3080   |-> cmpt 4482   Fn wfn 5596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-br 4424  df-opab 4483  df-mpt 4484  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-fun 5603  df-fn 5604

This theorem is referenced by:  mpt0  5723  fnmptfvd  6001  ralrnmpt  6047  fmpt  6059  fmpt2d  6069  f1ocnvd  6533  offval2  6563  ofrfval2  6564  mptelixpg  7571  fifo  7956  cantnflem1  8203  infmap2  8656  compssiso  8812  gruiun  9232  mptnn0fsupp  12216  mptnn0fsuppr  12218  seqof  12277  rlimi2  13578  prdsbas3  15379  prdsbascl  15381  prdsdsval2  15382  quslem  15449  fnmrc  15513  isofn  15680  pmtrrn  17098  pmtrfrn  17099  pmtrdifwrdellem2  17123  gsummptcl  17599  dprdwdOLD  17644  mptscmfsupp0  18153  ofco2  19475  pmatcollpw2lem  19800  neif  20115  tgrest  20174  cmpfi  20422  elptr2  20588  xkoptsub  20668  ptcmplem2  21067  ptcmplem3  21068  prdsxmetlem  21382  prdsxmslem2  21543  bcth3  22298  uniioombllem6  22545  itg2const  22697  ellimc2  22831  dvrec  22908  dvmptres3  22909  ulmss  23351  ulmdvlem1  23354  ulmdvlem2  23355  ulmdvlem3  23356  itgulm2  23363  psercn  23380  f1o3d  28232  f1od2  28316  psgnfzto1stlem  28622  rmulccn  28743  esumnul  28878  esum0  28879  gsumesum  28889  ofcfval2  28934  signsplypnf  29448  signsply0  29449  cdlemk56  34508  dicfnN  34721  hbtlem7  35955  refsumcn  37325  wessf1ornlem  37421  stoweidlem31  37833  stoweidlem59  37861  stirlinglem13  37889  dirkercncflem2  37907  fourierdlem62  37973  hoidmvlelem3  38324  dfafn5b  38534  lincresunit2  39922