Theorem fnmpt 6181

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

Syntax hints:   → wi 4   = wceq 1632   ∈ wcel 2139  ∀wral 3050  Vcvv 3340   ↦ cmpt 4881   Fn wfn 6044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-fun 6051  df-fn 6052

This theorem is referenced by:  mpt0  6182  fnmptfvd  6483  ralrnmpt  6531  fmpt  6544  fmpt2d  6556  f1ocnvd  7049  offval2  7079  ofrfval2  7080  mptelixpg  8111  fifo  8503  cantnflem1  8759  infmap2  9232  compssiso  9388  gruiun  9813  mptnn0fsupp  12991  mptnn0fsuppr  12993  seqof  13052  rlimi2  14444  prdsbas3  16343  prdsbascl  16345  prdsdsval2  16346  quslem  16405  fnmrc  16469  isofn  16636  pmtrrn  18077  pmtrfrn  18078  pmtrdifwrdellem2  18102  gsummptcl  18566  mptscmfsupp0  19130  ofco2  20459  pmatcollpw2lem  20784  neif  21106  tgrest  21165  cmpfi  21413  elptr2  21579  xkoptsub  21659  ptcmplem2  22058  ptcmplem3  22059  prdsxmetlem  22374  prdsxmslem2  22535  bcth3  23328  uniioombllem6  23556  itg2const  23706  ellimc2  23840  dvrec  23917  dvmptres3  23918  ulmss  24350  ulmdvlem1  24353  ulmdvlem2  24354  ulmdvlem3  24355  itgulm2  24362  psercn  24379  f1o3d  29740  f1od2  29808  psgnfzto1stlem  30159  rmulccn  30283  esumnul  30419  esum0  30420  gsumesum  30430  ofcfval2  30475  signsplypnf  30936  signsply0  30937  hgt750lemb  31043  matunitlindflem1  33718  matunitlindflem2  33719  cdlemk56  36761  dicfnN  36974  hbtlem7  38197  refsumcn  39688  wessf1ornlem  39870  choicefi  39891  axccdom  39915  fnmptd  39933  fsumsermpt  40314  liminfval2  40503  stoweidlem31  40751  stoweidlem59  40779  stirlinglem13  40806  dirkercncflem2  40824  fourierdlem62  40888  subsaliuncllem  41078  subsaliuncl  41079  hoidmvlelem3  41317  dfafn5b  41747  lincresunit2  42777