Theorem fnmpt 6638

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 3450	. . 3 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
2	1	ralimi 3074	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
3		mptfng.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
4	3	mptfng 6637	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴)
5	2, 4	sylib 218	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∀wral 3051  Vcvv 3429   ↦ cmpt 5166   Fn wfn 6493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-fun 6500  df-fn 6501

This theorem is referenced by:  fnmptd  6639  mpt0  6640  fnmptfvd  6993  ralrnmptw  7046  ralrnmpt  7048  fmpt  7062  fmpt2d  7077  f1ocnvd  7618  offval2  7651  ofrfval2  7652  mptcnfimad  7939  fsplitfpar  8068  mptelixpg  8883  fifo  9345  cantnflem1  9610  infmap2  10139  compssiso  10296  gruiun  10722  mptnn0fsupp  13959  mptnn0fsuppr  13961  seqof  14021  rlimi2  15476  prdsbas3  17444  prdsbascl  17446  prdsdsval2  17447  quslem  17507  fnmrc  17573  isofn  17742  ghmquskerco  19259  pmtrrn  19432  pmtrfrn  19433  pmtrdifwrdellem2  19457  gsummptcl  19942  mptscmfsupp0  20922  ofco2  22416  pmatcollpw2lem  22742  neif  23065  tgrest  23124  cmpfi  23373  elptr2  23539  xkoptsub  23619  ptcmplem2  24018  ptcmplem3  24019  prdsxmetlem  24333  prdsxmslem2  24494  bcth3  25298  uniioombllem6  25555  itg2const  25707  ellimc2  25844  dvrec  25922  dvmptres3  25923  ulmss  26362  ulmdvlem1  26365  ulmdvlem2  26366  ulmdvlem3  26367  itgulm2  26374  psercn  26391  tgjustr  28542  f1o3d  32699  f1od2  32792  psgnfzto1stlem  33161  frlmdim  33755  rmulccn  34072  esumnul  34192  esum0  34193  gsumesum  34203  ofcfval2  34248  signsplypnf  34694  signsply0  34695  hgt750lemb  34800  fineqvnttrclse  35268  wevgblacfn  35291  matunitlindflem1  37937  matunitlindflem2  37938  cdlemk56  41417  dicfnN  41629  hbtlem7  43553  refsumcn  45461  wessf1ornlem  45615  choicefi  45629  axccdom  45651  fsumsermpt  46009  liminfval2  46196  stoweidlem31  46459  stoweidlem59  46487  stirlinglem13  46514  dirkercncflem2  46532  fourierdlem62  46596  subsaliuncllem  46785  subsaliuncl  46786  hoidmvlelem3  47025  dfafn5b  47609  fundcmpsurinjlem2  47859  upgrimwlklem1  48373  lincresunit2  48954  isofnALT  49506