Theorem fnmpt 6622

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∀wral 3044  Vcvv 3436   ↦ cmpt 5173   Fn wfn 6477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-fun 6484  df-fn 6485

This theorem is referenced by:  fnmptd  6623  mpt0  6624  fnmptfvd  6975  ralrnmptw  7028  ralrnmpt  7030  fmpt  7044  fmpt2d  7058  f1ocnvd  7600  offval2  7633  ofrfval2  7634  mptcnfimad  7921  fsplitfpar  8051  mptelixpg  8862  fifo  9322  cantnflem1  9585  infmap2  10111  compssiso  10268  gruiun  10693  mptnn0fsupp  13904  mptnn0fsuppr  13906  seqof  13966  rlimi2  15421  prdsbas3  17385  prdsbascl  17387  prdsdsval2  17388  quslem  17447  fnmrc  17513  isofn  17682  ghmquskerco  19163  pmtrrn  19336  pmtrfrn  19337  pmtrdifwrdellem2  19361  gsummptcl  19846  mptscmfsupp0  20830  ofco2  22336  pmatcollpw2lem  22662  neif  22985  tgrest  23044  cmpfi  23293  elptr2  23459  xkoptsub  23539  ptcmplem2  23938  ptcmplem3  23939  prdsxmetlem  24254  prdsxmslem2  24415  bcth3  25229  uniioombllem6  25487  itg2const  25639  ellimc2  25776  dvrec  25857  dvmptres3  25858  ulmss  26304  ulmdvlem1  26307  ulmdvlem2  26308  ulmdvlem3  26309  itgulm2  26316  psercn  26334  tgjustr  28419  f1o3d  32569  f1od2  32663  psgnfzto1stlem  33042  frlmdim  33578  rmulccn  33895  esumnul  34015  esum0  34016  gsumesum  34026  ofcfval2  34071  signsplypnf  34518  signsply0  34519  hgt750lemb  34624  fineqvnttrclse  35077  wevgblacfn  35086  matunitlindflem1  37600  matunitlindflem2  37601  cdlemk56  40954  dicfnN  41166  hbtlem7  43102  refsumcn  45012  wessf1ornlem  45167  choicefi  45182  axccdom  45204  fsumsermpt  45564  liminfval2  45753  stoweidlem31  46016  stoweidlem59  46044  stirlinglem13  46071  dirkercncflem2  46089  fourierdlem62  46153  subsaliuncllem  46342  subsaliuncl  46343  hoidmvlelem3  46582  dfafn5b  47149  fundcmpsurinjlem2  47387  upgrimwlklem1  47885  lincresunit2  48467  isofnALT  49020