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 3465	. . 3 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
2	1	ralimi 3066	. 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 1540   ∈ wcel 2109  ∀wral 3044  Vcvv 3444   ↦ cmpt 5183   Fn wfn 6494

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 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-fun 6501  df-fn 6502

This theorem is referenced by:  fnmptd  6641  mpt0  6642  fnmptfvd  6995  ralrnmptw  7048  ralrnmpt  7050  fmpt  7064  fmpt2d  7078  f1ocnvd  7620  offval2  7653  ofrfval2  7654  mptcnfimad  7944  fsplitfpar  8074  mptelixpg  8885  fifo  9359  cantnflem1  9618  infmap2  10146  compssiso  10303  gruiun  10728  mptnn0fsupp  13938  mptnn0fsuppr  13940  seqof  14000  rlimi2  15456  prdsbas3  17420  prdsbascl  17422  prdsdsval2  17423  quslem  17482  fnmrc  17548  isofn  17717  ghmquskerco  19198  pmtrrn  19371  pmtrfrn  19372  pmtrdifwrdellem2  19396  gsummptcl  19881  mptscmfsupp0  20865  ofco2  22371  pmatcollpw2lem  22697  neif  23020  tgrest  23079  cmpfi  23328  elptr2  23494  xkoptsub  23574  ptcmplem2  23973  ptcmplem3  23974  prdsxmetlem  24289  prdsxmslem2  24450  bcth3  25264  uniioombllem6  25522  itg2const  25674  ellimc2  25811  dvrec  25892  dvmptres3  25893  ulmss  26339  ulmdvlem1  26342  ulmdvlem2  26343  ulmdvlem3  26344  itgulm2  26351  psercn  26369  tgjustr  28454  f1o3d  32601  f1od2  32694  psgnfzto1stlem  33072  frlmdim  33600  rmulccn  33911  esumnul  34031  esum0  34032  gsumesum  34042  ofcfval2  34087  signsplypnf  34534  signsply0  34535  hgt750lemb  34640  wevgblacfn  35089  matunitlindflem1  37603  matunitlindflem2  37604  cdlemk56  40958  dicfnN  41170  hbtlem7  43107  refsumcn  45017  wessf1ornlem  45172  choicefi  45187  axccdom  45209  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  47890  lincresunit2  48460  isofnALT  49013