Theorem fnmpt 6630

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ∀wral 3049  Vcvv 3438   ↦ cmpt 5177   Fn wfn 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-fun 6492  df-fn 6493

This theorem is referenced by:  fnmptd  6631  mpt0  6632  fnmptfvd  6984  ralrnmptw  7037  ralrnmpt  7039  fmpt  7053  fmpt2d  7067  f1ocnvd  7607  offval2  7640  ofrfval2  7641  mptcnfimad  7928  fsplitfpar  8058  mptelixpg  8871  fifo  9333  cantnflem1  9596  infmap2  10125  compssiso  10282  gruiun  10708  mptnn0fsupp  13918  mptnn0fsuppr  13920  seqof  13980  rlimi2  15435  prdsbas3  17399  prdsbascl  17401  prdsdsval2  17402  quslem  17462  fnmrc  17528  isofn  17697  ghmquskerco  19211  pmtrrn  19384  pmtrfrn  19385  pmtrdifwrdellem2  19409  gsummptcl  19894  mptscmfsupp0  20876  ofco2  22393  pmatcollpw2lem  22719  neif  23042  tgrest  23101  cmpfi  23350  elptr2  23516  xkoptsub  23596  ptcmplem2  23995  ptcmplem3  23996  prdsxmetlem  24310  prdsxmslem2  24471  bcth3  25285  uniioombllem6  25543  itg2const  25695  ellimc2  25832  dvrec  25913  dvmptres3  25914  ulmss  26360  ulmdvlem1  26363  ulmdvlem2  26364  ulmdvlem3  26365  itgulm2  26372  psercn  26390  tgjustr  28495  f1o3d  32653  f1od2  32747  psgnfzto1stlem  33131  frlmdim  33717  rmulccn  34034  esumnul  34154  esum0  34155  gsumesum  34165  ofcfval2  34210  signsplypnf  34656  signsply0  34657  hgt750lemb  34762  fineqvnttrclse  35229  wevgblacfn  35252  matunitlindflem1  37756  matunitlindflem2  37757  cdlemk56  41170  dicfnN  41382  hbtlem7  43309  refsumcn  45217  wessf1ornlem  45371  choicefi  45386  axccdom  45408  fsumsermpt  45767  liminfval2  45954  stoweidlem31  46217  stoweidlem59  46245  stirlinglem13  46272  dirkercncflem2  46290  fourierdlem62  46354  subsaliuncllem  46543  subsaliuncl  46544  hoidmvlelem3  46783  dfafn5b  47349  fundcmpsurinjlem2  47587  upgrimwlklem1  48085  lincresunit2  48666  isofnALT  49218