Theorem fnmpt 6460

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  ∀wral 3106  Vcvv 3441   ↦ cmpt 5110   Fn wfn 6319

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-fun 6326  df-fn 6327

This theorem is referenced by:  fnmptd  6461  mpt0  6462  fnmptfvd  6788  ralrnmptw  6837  ralrnmpt  6839  fmpt  6851  fmpt2d  6864  f1ocnvd  7376  offval2  7406  ofrfval2  7407  fsplitfpar  7797  mptelixpg  8482  fifo  8880  cantnflem1  9136  infmap2  9629  compssiso  9785  gruiun  10210  mptnn0fsupp  13360  mptnn0fsuppr  13362  seqof  13423  rlimi2  14863  prdsbas3  16746  prdsbascl  16748  prdsdsval2  16749  quslem  16808  fnmrc  16870  isofn  17037  pmtrrn  18577  pmtrfrn  18578  pmtrdifwrdellem2  18602  gsummptcl  19080  mptscmfsupp0  19692  ofco2  21056  pmatcollpw2lem  21382  neif  21705  tgrest  21764  cmpfi  22013  elptr2  22179  xkoptsub  22259  ptcmplem2  22658  ptcmplem3  22659  prdsxmetlem  22975  prdsxmslem2  23136  bcth3  23935  uniioombllem6  24192  itg2const  24344  ellimc2  24480  dvrec  24558  dvmptres3  24559  ulmss  24992  ulmdvlem1  24995  ulmdvlem2  24996  ulmdvlem3  24997  itgulm2  25004  psercn  25021  tgjustr  26268  f1o3d  30386  f1od2  30483  psgnfzto1stlem  30792  frlmdim  31097  rmulccn  31281  esumnul  31417  esum0  31418  gsumesum  31428  ofcfval2  31473  signsplypnf  31930  signsply0  31931  hgt750lemb  32037  matunitlindflem1  35053  matunitlindflem2  35054  cdlemk56  38267  dicfnN  38479  hbtlem7  40069  refsumcn  41659  wessf1ornlem  41811  choicefi  41829  axccdom  41853  fsumsermpt  42221  liminfval2  42410  stoweidlem31  42673  stoweidlem59  42701  stirlinglem13  42728  dirkercncflem2  42746  fourierdlem62  42810  subsaliuncllem  42997  subsaliuncl  42998  hoidmvlelem3  43236  dfafn5b  43717  fundcmpsurinjlem2  43916  lincresunit2  44887