Theorem fnmpti 6712

Description: The maps-to notation defines a function with domain. (Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)

Hypotheses

Ref	Expression
fnmpti.1	⊢ 𝐵 ∈ V
fnmpti.2	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)

Assertion

Ref	Expression
fnmpti	⊢ 𝐹 Fn 𝐴

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)

Proof of Theorem fnmpti

Step	Hyp	Ref	Expression
1		fnmpti.1	. . 3 ⊢ 𝐵 ∈ V
2	1	rgenw 3084	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 ∈ V
3		fnmpti.2	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
4	3	mptfng 6708	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴)
5	2, 4	mpbi 233	1 ⊢ 𝐹 Fn 𝐴

This proof depends on syntax axioms:   = 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:  dmmpti  6713  fconst  6798  dffn5  6974  idref  7181  eufnfv  7266  offn  7738  caofinvl  7757  fo1st  8055  fo2nd  8056  reldmOLD  8090  fimaproj  8189  mapsnf1o2  8960  unfilem2  9336  fidomdm  9361  noinfep  9698  ssttrcl  9753  ttrcltr  9754  ttrclselem2  9764  aceq3lem  10238  dfac4  10240  ackbij2lem2  10356  cfslb2n  10385  axcc2lem  10553  dmct  10641  dmctOLD  10642  konigthlem  10692  rankcf  10901  tskuni  10907  seqf1o  14226  ccatlen  14761  ccatvalfn  14767  swrdlen  14837  swrdwrdsymb  14854  swrdswrd  14896  sqrtf  15575  mptfzshft  15988  efcvgfsum  16296  prmreclem2  17139  1arith  17149  vdwlem6  17208  vdwlem8  17210  slotfn  17406  topnfn  17646  fnmre  17811  cidffn  17902  cidfn  17903  funcres  18121  initofn  18212  termofn  18213  zeroofn  18214  yonedainv  18505  fn0g  18893  smndex1igid  19152  smndex1igidOLD  19153  smndex1n0mnd  19161  grpinvfn  19242  cycsubmel  19465  conjnmz  19516  ghmquskerco  19549  psgnfn  19766  odf  19802  sylow1lem4  19866  pgpssslw  19879  sylow2blem3  19887  sylow3lem2  19893  cygctb  20157  dprd2da  20309  fnmgp  20413  zrinitorngc  20945  zrtermorngc  20946  zrtermoringc  20978  rrgsupp  21004  rlmfn  21516  frlmup4  22162  asclfn  22243  evlslem1  22446  evlsvvval  22457  psdmplcl  22538  psdadd  22539  psdmul  22542  psdmvr  22545  mdetrlin  22972  matunitlindflem1  23049  fncld  23395  hauseqlcld  24020  kqf  24121  filunirn  24256  fmf  24319  txflf  24380  clsnsg  24484  tgpconncomp  24487  qustgpopn  24494  qustgplem  24495  ustfn  24576  xmetunirn  24711  met1stc  24895  rrxmvallem  25780  ovolf  25858  vitali  25989  i1fmulc  26079  mbfi1fseqlem4  26094  itg2seq  26118  itg2monolem1  26126  i1fibl  26183  fncpn  26308  lhop1lem  26388  mdegxrf  26441  aannenlem3  26714  efabl  26935  logccv  27048  gausslemma2dlem1  27750  padicabvf  28015  mpteleeOLD  29530  wlkiswwlks2lem1  30515  clwlkclwwlklem2a2  30641  grpoinvf  31191  occllem  31962  pjfni  32360  pjmfn  32374  rnbra  32766  bra11  32767  kbass2  32776  hmopidmchi  32810  xppreima2  33343  abfmpunirn  33344  psgnfzto1stlem  33760  elrspunidl  34082  locfinreflem  34583  zarclsint  34615  zar0ring  34621  rhmpreimacn  34628  ofcfn  34843  sxbrsigalem3  35015  eulerpartgbij  35115  sseqfv1  35132  sseqfn  35133  sseqf  35135  sseqfv2  35137  signstlen  35307  kardfn  35960  maxssj0  36047  vonf1oonfo  36090  msubrn  36502  msrf  36515  mirimanoffr  36668  faclimlem1  36723  weiunlem  37466  bj-evalfn  38264  bj-inftyexpitaufo  38391  poimirlem30  38836  mblfinlem2  38844  volsupnfl  38851  cnambfre  38854  itg2addnclem2  38858  itg2addnclem3  38859  ftc1anclem5  38883  ftc1anclem7  38885  sdclem2  38942  prdsbnd2  38995  rrncmslem  39032  diafn  42357  cdlemm10N  42441  dibfna  42477  lcfrlem9  42873  mapd1o  42971  hdmapfnN  43152  hgmapfnN  43211  fsuppind  43884  rmxypairf1o  44184  hbtlem6  44396  dgraaf  44414  cytpfn  44464  tfsconcatrev  44611  ntrf  45384  uzmptshftfval  45591  binomcxplemrat  45595  addrfn  45714  subrfn  45715  mulvfn  45716  limsup10exlem  47055  liminfvalxr  47066  fourierdlem62  47451  fourierdlem70  47459  fourierdlem71  47460  cjnpoly  48212  fmtnorn  48892  tposideq  50332  cicfn  50487  fucofn22  50793  fucoid  50801  dfinito4  50967  crosspaltd  51394  crossp3d  51395  veronesevrowd  51407  veronesematrowd  51409  veroquadmodzerod  51412