Theorem fnmpt 6632

Description: The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013.)

Hypothesis

Ref	Expression
mptfng.1	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)

Assertion

Ref	Expression
fnmpt	⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐹 Fn 𝐴)

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)   𝑉(𝑥)

Proof of Theorem fnmpt

Step	Hyp	Ref	Expression
1		elex 3461	. . 3 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
2	1	ralimi 3073	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
3		mptfng.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
4	3	mptfng 6631	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴)
5	2, 4	sylib 218	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ∀wral 3051  Vcvv 3440   ↦ cmpt 5179   Fn wfn 6487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-fun 6494  df-fn 6495

This theorem is referenced by:  fnmptd  6633  mpt0  6634  fnmptfvd  6986  ralrnmptw  7039  ralrnmpt  7041  fmpt  7055  fmpt2d  7069  f1ocnvd  7609  offval2  7642  ofrfval2  7643  mptcnfimad  7930  fsplitfpar  8060  mptelixpg  8873  fifo  9335  cantnflem1  9598  infmap2  10127  compssiso  10284  gruiun  10710  mptnn0fsupp  13920  mptnn0fsuppr  13922  seqof  13982  rlimi2  15437  prdsbas3  17401  prdsbascl  17403  prdsdsval2  17404  quslem  17464  fnmrc  17530  isofn  17699  ghmquskerco  19213  pmtrrn  19386  pmtrfrn  19387  pmtrdifwrdellem2  19411  gsummptcl  19896  mptscmfsupp0  20878  ofco2  22395  pmatcollpw2lem  22721  neif  23044  tgrest  23103  cmpfi  23352  elptr2  23518  xkoptsub  23598  ptcmplem2  23997  ptcmplem3  23998  prdsxmetlem  24312  prdsxmslem2  24473  bcth3  25287  uniioombllem6  25545  itg2const  25697  ellimc2  25834  dvrec  25915  dvmptres3  25916  ulmss  26362  ulmdvlem1  26365  ulmdvlem2  26366  ulmdvlem3  26367  itgulm2  26374  psercn  26392  tgjustr  28546  f1o3d  32704  f1od2  32798  psgnfzto1stlem  33182  frlmdim  33768  rmulccn  34085  esumnul  34205  esum0  34206  gsumesum  34216  ofcfval2  34261  signsplypnf  34707  signsply0  34708  hgt750lemb  34813  fineqvnttrclse  35280  wevgblacfn  35303  matunitlindflem1  37817  matunitlindflem2  37818  cdlemk56  41241  dicfnN  41453  hbtlem7  43377  refsumcn  45285  wessf1ornlem  45439  choicefi  45454  axccdom  45476  fsumsermpt  45835  liminfval2  46022  stoweidlem31  46285  stoweidlem59  46313  stirlinglem13  46340  dirkercncflem2  46358  fourierdlem62  46422  subsaliuncllem  46611  subsaliuncl  46612  hoidmvlelem3  46851  dfafn5b  47417  fundcmpsurinjlem2  47655  upgrimwlklem1  48153  lincresunit2  48734  isofnALT  49286