Theorem fnmpt 6640

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∀wral 3052  Vcvv 3442   ↦ cmpt 5181   Fn wfn 6495

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 5243  ax-pr 5379

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-fun 6502  df-fn 6503

This theorem is referenced by:  fnmptd  6641  mpt0  6642  fnmptfvd  6995  ralrnmptw  7048  ralrnmpt  7050  fmpt  7064  fmpt2d  7079  f1ocnvd  7619  offval2  7652  ofrfval2  7653  mptcnfimad  7940  fsplitfpar  8070  mptelixpg  8885  fifo  9347  cantnflem1  9610  infmap2  10139  compssiso  10296  gruiun  10722  mptnn0fsupp  13932  mptnn0fsuppr  13934  seqof  13994  rlimi2  15449  prdsbas3  17413  prdsbascl  17415  prdsdsval2  17416  quslem  17476  fnmrc  17542  isofn  17711  ghmquskerco  19228  pmtrrn  19401  pmtrfrn  19402  pmtrdifwrdellem2  19426  gsummptcl  19911  mptscmfsupp0  20893  ofco2  22410  pmatcollpw2lem  22736  neif  23059  tgrest  23118  cmpfi  23367  elptr2  23533  xkoptsub  23613  ptcmplem2  24012  ptcmplem3  24013  prdsxmetlem  24327  prdsxmslem2  24488  bcth3  25302  uniioombllem6  25560  itg2const  25712  ellimc2  25849  dvrec  25930  dvmptres3  25931  ulmss  26377  ulmdvlem1  26380  ulmdvlem2  26381  ulmdvlem3  26382  itgulm2  26389  psercn  26407  tgjustr  28562  f1o3d  32720  f1od2  32813  psgnfzto1stlem  33198  frlmdim  33793  rmulccn  34110  esumnul  34230  esum0  34231  gsumesum  34241  ofcfval2  34286  signsplypnf  34732  signsply0  34733  hgt750lemb  34838  fineqvnttrclse  35306  wevgblacfn  35329  matunitlindflem1  37871  matunitlindflem2  37872  cdlemk56  41351  dicfnN  41563  hbtlem7  43486  refsumcn  45394  wessf1ornlem  45548  choicefi  45562  axccdom  45584  fsumsermpt  45943  liminfval2  46130  stoweidlem31  46393  stoweidlem59  46421  stirlinglem13  46448  dirkercncflem2  46466  fourierdlem62  46530  subsaliuncllem  46719  subsaliuncl  46720  hoidmvlelem3  46959  dfafn5b  47525  fundcmpsurinjlem2  47763  upgrimwlklem1  48261  lincresunit2  48842  isofnALT  49394