Theorem fnmpt 6020

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 3212	. . 3 |- ( B e. V -> B e. _V )
2	1	ralimi 2952	. 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 6019	. 2 |- ( A. x e. A B e. _V <-> F Fn A )
5	2, 4	sylib 208	1 |- ( A. x e. A B e. V -> F Fn A )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990   A.wral 2912   _Vcvv 3200   |-> cmpt 4729   Fn wfn 5883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-fun 5890  df-fn 5891

This theorem is referenced by:  mpt0  6021  fnmptfvd  6320  ralrnmpt  6368  fmpt  6381  fmpt2d  6393  f1ocnvd  6884  offval2  6914  ofrfval2  6915  mptelixpg  7945  fifo  8338  cantnflem1  8586  infmap2  9040  compssiso  9196  gruiun  9621  mptnn0fsupp  12797  mptnn0fsuppr  12799  seqof  12858  rlimi2  14245  prdsbas3  16141  prdsbascl  16143  prdsdsval2  16144  quslem  16203  fnmrc  16267  isofn  16435  pmtrrn  17877  pmtrfrn  17878  pmtrdifwrdellem2  17902  gsummptcl  18366  mptscmfsupp0  18928  ofco2  20257  pmatcollpw2lem  20582  neif  20904  tgrest  20963  cmpfi  21211  elptr2  21377  xkoptsub  21457  ptcmplem2  21857  ptcmplem3  21858  prdsxmetlem  22173  prdsxmslem2  22334  bcth3  23128  uniioombllem6  23356  itg2const  23507  ellimc2  23641  dvrec  23718  dvmptres3  23719  ulmss  24151  ulmdvlem1  24154  ulmdvlem2  24155  ulmdvlem3  24156  itgulm2  24163  psercn  24180  f1o3d  29431  f1od2  29499  psgnfzto1stlem  29850  rmulccn  29974  esumnul  30110  esum0  30111  gsumesum  30121  ofcfval2  30166  signsplypnf  30627  signsply0  30628  hgt750lemb  30734  matunitlindflem1  33405  matunitlindflem2  33406  cdlemk56  36259  dicfnN  36472  hbtlem7  37695  refsumcn  39189  wessf1ornlem  39371  choicefi  39392  axccdom  39416  fnmptd  39434  fsumsermpt  39811  liminfval2  40000  stoweidlem31  40248  stoweidlem59  40276  stirlinglem13  40303  dirkercncflem2  40321  fourierdlem62  40385  subsaliuncllem  40575  subsaliuncl  40576  hoidmvlelem3  40811  dfafn5b  41241  lincresunit2  42267