Theorem fnmpt 6708

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  ∀wral 3058  Vcvv 3477   ↦ cmpt 5230   Fn wfn 6557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-fun 6564  df-fn 6565

This theorem is referenced by:  fnmptd  6709  mpt0  6710  fnmptfvd  7060  ralrnmptw  7113  ralrnmpt  7115  fmpt  7129  fmpt2d  7143  f1ocnvd  7683  offval2  7716  ofrfval2  7717  mptcnfimad  8009  fsplitfpar  8141  mptelixpg  8973  fifo  9469  cantnflem1  9726  infmap2  10254  compssiso  10411  gruiun  10836  mptnn0fsupp  14034  mptnn0fsuppr  14036  seqof  14096  rlimi2  15546  prdsbas3  17527  prdsbascl  17529  prdsdsval2  17530  quslem  17589  fnmrc  17651  isofn  17822  ghmquskerco  19314  pmtrrn  19489  pmtrfrn  19490  pmtrdifwrdellem2  19514  gsummptcl  19999  mptscmfsupp0  20941  ofco2  22472  pmatcollpw2lem  22798  neif  23123  tgrest  23182  cmpfi  23431  elptr2  23597  xkoptsub  23677  ptcmplem2  24076  ptcmplem3  24077  prdsxmetlem  24393  prdsxmslem2  24557  bcth3  25378  uniioombllem6  25636  itg2const  25789  ellimc2  25926  dvrec  26007  dvmptres3  26008  ulmss  26454  ulmdvlem1  26457  ulmdvlem2  26458  ulmdvlem3  26459  itgulm2  26466  psercn  26484  tgjustr  28496  f1o3d  32643  f1od2  32738  psgnfzto1stlem  33102  frlmdim  33638  rmulccn  33888  esumnul  34028  esum0  34029  gsumesum  34039  ofcfval2  34084  signsplypnf  34543  signsply0  34544  hgt750lemb  34649  wevgblacfn  35092  matunitlindflem1  37602  matunitlindflem2  37603  cdlemk56  40953  dicfnN  41165  hbtlem7  43113  refsumcn  44967  wessf1ornlem  45127  choicefi  45142  axccdom  45164  fsumsermpt  45534  liminfval2  45723  stoweidlem31  45986  stoweidlem59  46014  stirlinglem13  46041  dirkercncflem2  46059  fourierdlem62  46123  subsaliuncllem  46312  subsaliuncl  46313  hoidmvlelem3  46552  dfafn5b  47110  fundcmpsurinjlem2  47323  lincresunit2  48323