Theorem fnmpt 6709

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  ∀wral 3080  Vcvv 3454   ↦ cmpt 5192   Fn wfn 6561

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-fun 6568  df-fn 6569

This theorem is used by:  fnmptd  6710  mpt0  6711  fnmptfvd  7071  ralrnmptw  7126  ralrnmpt  7128  fmpt  7142  fmpt2d  7157  f1ocnvd  7704  offval2  7745  ofrfval2  7746  mptcnfimad  8032  f1od2  8145  fsplitfpar  8166  mptelixpg  9001  fifo  9461  cantnflem1  9727  infmap2  10334  compssiso  10491  gruiun  10923  mptnn0fsupp  14180  mptnn0fsuppr  14182  seqof  14242  sgnrn  15294  rlimi2  15725  prdsbas3  17702  prdsbascl  17704  prdsdsval2  17705  quslem  17765  fnmrc  17831  isofn  18000  ghmquskerco  19549  pmtrrn  19722  pmtrfrn  19723  pmtrdifwrdellem2  19747  gsummptcl  20232  mptscmfsupp0  21253  ofco2  22821  matunitlindflem1  23049  matunitlindflem2  23050  pmatcollpw2lem  23150  neif  23473  tgrest  23532  cmpfi  23781  elptr2  23948  xkoptsub  24028  ptcmplem2  24427  ptcmplem3  24428  prdsxmetlem  24742  prdsxmslem2  24903  bcth3  25707  uniioombllem6  25964  itg2const  26116  ellimc2  26252  dvrec  26330  dvmptres3  26331  ulmss  26781  ulmdvlem1  26784  ulmdvlem2  26785  ulmdvlem3  26786  itgulm2  26793  psercn  26810  tgjustr  28993  f1o3d  33318  psgnfzto1stlem  33760  frlmdim  34354  rmulccn  34671  esumnul  34791  esum0  34792  gsumesum  34802  ofcfval2  34847  signsplypnf  35290  signsply0  35291  hgt750lemb  35396  fineqvnttrclse  35933  wevgblacfn  36080  mirimanoffr  36668  cdlemk56  42294  dicfnN  42506  hbtlem7  44392  refsumcn  46321  wessf1ornlem  46473  choicefi  46487  axccdom  46508  fsumsermpt  46864  liminfval2  47051  stoweidlem31  47314  stoweidlem59  47342  stirlinglem13  47369  dirkercncflem2  47387  fourierdlem62  47451  subsaliuncllem  47640  subsaliuncl  47641  hoidmvlelem3  47880  dfafn5b  48504  fundcmpsurinjlem2  48754  upgrimwlklem1  49268  lincresunit2  49921  isofnALT  50476