Theorem fnmpt 6633

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∀wral 3052  Vcvv 3430   ↦ cmpt 5167   Fn wfn 6488

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 2709  ax-sep 5232  ax-pr 5371

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-fun 6495  df-fn 6496

This theorem is referenced by:  fnmptd  6634  mpt0  6635  fnmptfvd  6988  ralrnmptw  7041  ralrnmpt  7043  fmpt  7057  fmpt2d  7072  f1ocnvd  7612  offval2  7645  ofrfval2  7646  mptcnfimad  7933  fsplitfpar  8062  mptelixpg  8877  fifo  9339  cantnflem1  9604  infmap2  10133  compssiso  10290  gruiun  10716  mptnn0fsupp  13953  mptnn0fsuppr  13955  seqof  14015  rlimi2  15470  prdsbas3  17438  prdsbascl  17440  prdsdsval2  17441  quslem  17501  fnmrc  17567  isofn  17736  ghmquskerco  19253  pmtrrn  19426  pmtrfrn  19427  pmtrdifwrdellem2  19451  gsummptcl  19936  mptscmfsupp0  20916  ofco2  22429  pmatcollpw2lem  22755  neif  23078  tgrest  23137  cmpfi  23386  elptr2  23552  xkoptsub  23632  ptcmplem2  24031  ptcmplem3  24032  prdsxmetlem  24346  prdsxmslem2  24507  bcth3  25311  uniioombllem6  25568  itg2const  25720  ellimc2  25857  dvrec  25935  dvmptres3  25936  ulmss  26378  ulmdvlem1  26381  ulmdvlem2  26382  ulmdvlem3  26383  itgulm2  26390  psercn  26407  tgjustr  28559  f1o3d  32717  f1od2  32810  psgnfzto1stlem  33179  frlmdim  33774  rmulccn  34091  esumnul  34211  esum0  34212  gsumesum  34222  ofcfval2  34267  signsplypnf  34713  signsply0  34714  hgt750lemb  34819  fineqvnttrclse  35287  wevgblacfn  35310  matunitlindflem1  37954  matunitlindflem2  37955  cdlemk56  41434  dicfnN  41646  hbtlem7  43574  refsumcn  45482  wessf1ornlem  45636  choicefi  45650  axccdom  45672  fsumsermpt  46030  liminfval2  46217  stoweidlem31  46480  stoweidlem59  46508  stirlinglem13  46535  dirkercncflem2  46553  fourierdlem62  46617  subsaliuncllem  46806  subsaliuncl  46807  hoidmvlelem3  47046  dfafn5b  47624  fundcmpsurinjlem2  47874  upgrimwlklem1  48388  lincresunit2  48969  isofnALT  49521