Theorem fnmpt 6625

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  ∀wral 3053  Vcvv 3431   ↦ cmpt 5153   Fn wfn 6480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-fun 6487  df-fn 6488

This theorem is referenced by:  fnmptd  6626  mpt0  6627  fnmptfvd  6982  ralrnmptw  7035  ralrnmpt  7037  fmpt  7051  fmpt2d  7066  f1ocnvd  7607  offval2  7640  ofrfval2  7641  mptcnfimad  7928  fsplitfpar  8057  mptelixpg  8873  fifo  9335  cantnflem1  9601  infmap2  10130  compssiso  10287  gruiun  10713  mptnn0fsupp  13950  mptnn0fsuppr  13952  seqof  14012  rlimi2  15467  prdsbas3  17435  prdsbascl  17437  prdsdsval2  17438  quslem  17498  fnmrc  17564  isofn  17733  ghmquskerco  19250  pmtrrn  19423  pmtrfrn  19424  pmtrdifwrdellem2  19448  gsummptcl  19933  mptscmfsupp0  20917  ofco2  22434  pmatcollpw2lem  22760  neif  23083  tgrest  23142  cmpfi  23391  elptr2  23557  xkoptsub  23637  ptcmplem2  24036  ptcmplem3  24037  prdsxmetlem  24351  prdsxmslem2  24512  bcth3  25316  uniioombllem6  25573  itg2const  25725  ellimc2  25862  dvrec  25940  dvmptres3  25941  ulmss  26380  ulmdvlem1  26383  ulmdvlem2  26384  ulmdvlem3  26385  itgulm2  26392  psercn  26409  tgjustr  28560  f1o3d  32718  f1od2  32811  psgnfzto1stlem  33181  frlmdim  33795  rmulccn  34112  esumnul  34232  esum0  34233  gsumesum  34243  ofcfval2  34288  signsplypnf  34734  signsply0  34735  hgt750lemb  34840  fineqvnttrclse  35305  wevgblacfn  35337  matunitlindflem1  37983  matunitlindflem2  37984  cdlemk56  41463  dicfnN  41675  hbtlem7  43570  refsumcn  45478  wessf1ornlem  45632  choicefi  45646  axccdom  45667  fsumsermpt  46024  liminfval2  46211  stoweidlem31  46474  stoweidlem59  46502  stirlinglem13  46529  dirkercncflem2  46547  fourierdlem62  46611  subsaliuncllem  46800  subsaliuncl  46801  hoidmvlelem3  47040  dfafn5b  47624  fundcmpsurinjlem2  47874  upgrimwlklem1  48388  lincresunit2  48969  isofnALT  49521