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  32570  f1od2  32664  psgnfzto1stlem  33043  frlmdim  33584  rmulccn  33901  esumnul  34021  esum0  34022  gsumesum  34032  ofcfval2  34077  signsplypnf  34524  signsply0  34525  hgt750lemb  34630  fineqvnttrclse  35083  wevgblacfn  35092  matunitlindflem1  37606  matunitlindflem2  37607  cdlemk56  40960  dicfnN  41172  hbtlem7  43108  refsumcn  45018  wessf1ornlem  45173  choicefi  45188  axccdom  45210  fsumsermpt  45570  liminfval2  45759  stoweidlem31  46022  stoweidlem59  46050  stirlinglem13  46077  dirkercncflem2  46095  fourierdlem62  46159  subsaliuncllem  46348  subsaliuncl  46349  hoidmvlelem3  46588  dfafn5b  47155  fundcmpsurinjlem2  47393  upgrimwlklem1  47891  lincresunit2  48473  isofnALT  49026