Theorem fnmpt 5525

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 2971	. . 3 |- ( B e. V -> B e. _V )
2	1	ralimi 2781	. 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 5524	. 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 1362   e. wcel 1755   A.wral 2705   _Vcvv 2962   e. cmpt 4338   Fn wfn 5401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-fun 5408  df-fn 5409

This theorem is referenced by:  mpt0  5526  fnmptfvd  5794  ralrnmpt  5840  fmpt  5852  fmpt2d  5860  f1ocnvd  6298  offval2  6325  ofrfval2  6326  mptelixpg  7288  fifo  7670  cantnflem1  7885  infmap2  8375  compssiso  8531  gruiun  8953  seqof  11846  rlimi2  12975  rlimmptrcl  13068  prdsbas3  14401  prdsbascl  14403  prdsdsval2  14404  divslem  14463  fnmrc  14527  pmtrrn  15942  pmtrfrn  15943  pmtrdifwrdellem2  15967  gsummptcl  16431  dprdwd  16468  dprdwdOLD  16474  ofco2  18173  neif  18545  tgrest  18604  cmpfi  18852  elptr2  18988  xkoptsub  19068  ptcmplem2  19466  ptcmplem3  19467  prdsxmetlem  19784  prdsxmslem2  19945  bcth3  20683  uniioombllem6  20909  itg2const  21059  iblcnlem  21107  ellimc2  21193  dvrec  21270  dvmptres3  21271  ulmss  21746  ulmdvlem1  21749  ulmdvlem2  21750  ulmdvlem3  21751  itgulm2  21758  psercn  21775  f1o3d  25771  f1od2  25847  rmulccn  26211  esumnul  26355  esum0  26356  ofcfval2  26399  signsplypnf  26798  signsply0  26799  signstlen  26815  hbtlem7  29323  refsumcn  29594  stoweidlem31  29669  stoweidlem59  29697  stirlinglem13  29724  dfafn5b  29910  lincresunit2  30718  cdlemk56  34185  dicfnN  34398