Theorem fnmpt 6676

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ∀wral 3078  Vcvv 3453   ↦ cmpt 5190   Fn wfn 6532

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-pr 5402

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 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-fun 6539  df-fn 6540

This theorem is used by:  fnmptd  6677  mpt0  6678  fnmptfvd  7037  ralrnmptw  7091  ralrnmpt  7093  fmpt  7107  fmpt2d  7122  f1ocnvd  7669  offval2  7702  ofrfval2  7703  mptcnfimad  7987  fsplitfpar  8119  mptelixpg  8946  fifo  9406  cantnflem1  9672  infmap2  10223  compssiso  10380  gruiun  10812  mptnn0fsupp  14065  mptnn0fsuppr  14067  seqof  14127  sgnrn  15175  rlimi2  15605  prdsbas3  17572  prdsbascl  17574  prdsdsval2  17575  quslem  17635  fnmrc  17701  isofn  17870  ghmquskerco  19417  pmtrrn  19590  pmtrfrn  19591  pmtrdifwrdellem2  19615  gsummptcl  20100  mptscmfsupp0  21117  ofco2  22679  matunitlindflem1  22907  matunitlindflem2  22908  pmatcollpw2lem  23008  neif  23331  tgrest  23390  cmpfi  23639  elptr2  23806  xkoptsub  23886  ptcmplem2  24285  ptcmplem3  24286  prdsxmetlem  24600  prdsxmslem2  24761  bcth3  25565  uniioombllem6  25822  itg2const  25974  ellimc2  26111  dvrec  26189  dvmptres3  26190  ulmss  26640  ulmdvlem1  26643  ulmdvlem2  26644  ulmdvlem3  26645  itgulm2  26652  psercn  26669  tgjustr  28823  f1o3d  33107  f1od2  33198  psgnfzto1stlem  33548  frlmdim  34129  rmulccn  34446  esumnul  34566  esum0  34567  gsumesum  34577  ofcfval2  34622  signsplypnf  35066  signsply0  35067  hgt750lemb  35172  fineqvnttrclse  35658  wevgblacfn  35716  cdlemk56  41852  dicfnN  42064  hbtlem7  43974  refsumcn  45872  wessf1ornlem  46025  choicefi  46039  axccdom  46060  fsumsermpt  46417  liminfval2  46604  stoweidlem31  46867  stoweidlem59  46895  stirlinglem13  46922  dirkercncflem2  46940  fourierdlem62  47004  subsaliuncllem  47193  subsaliuncl  47194  hoidmvlelem3  47433  dfafn5b  48057  fundcmpsurinjlem2  48307  upgrimwlklem1  48821  lincresunit2  49416  isofnALT  49965