Theorem fnmpti 6690

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 3083	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 ∈ V
3		fnmpti.2	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
4	3	mptfng 6686	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴)
5	2, 4	mpbi 233	1 ⊢ 𝐹 Fn 𝐴

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2146  ∀wral 3079  Vcvv 3453   ↦ cmpt 5188   Fn wfn 6541

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-pr 5394

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-br 5106  df-opab 5170  df-mpt 5189  df-id 5549  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-fun 6548  df-fn 6549

This theorem is used by:  dmmpti  6691  fconst  6776  dffn5  6951  idref  7157  eufnfv  7242  offn  7713  caofinvl  7732  fo1st  8028  fo2nd  8029  reldmOLD  8063  fimaproj  8162  mapsnf1o2  8933  unfilem2  9309  fidomdm  9334  noinfep  9671  ssttrcl  9726  ttrcltr  9727  ttrclselem2  9737  aceq3lem  10209  dfac4  10211  ackbij2lem2  10327  cfslb2n  10356  axcc2lem  10524  dmct  10612  dmctOLD  10613  konigthlem  10663  rankcf  10872  tskuni  10878  seqf1o  14196  ccatlen  14730  ccatvalfn  14736  swrdlen  14806  swrdwrdsymb  14823  swrdswrd  14865  sqrtf  15543  mptfzshft  15956  efcvgfsum  16264  prmreclem2  17107  1arith  17117  vdwlem6  17176  vdwlem8  17178  slotfn  17374  topnfn  17608  fnmre  17773  cidffn  17864  cidfn  17865  funcres  18083  initofn  18174  termofn  18175  zeroofn  18176  yonedainv  18467  fn0g  18855  smndex1igid  19114  smndex1igidOLD  19115  smndex1n0mnd  19123  grpinvfn  19204  cycsubmel  19427  conjnmz  19478  ghmquskerco  19510  psgnfn  19727  odf  19763  sylow1lem4  19827  pgpssslw  19840  sylow2blem3  19848  sylow3lem2  19854  cygctb  20118  dprd2da  20270  fnmgp  20374  zrinitorngc  20906  zrtermorngc  20907  zrtermoringc  20939  rrgsupp  20965  rlmfn  21477  frlmup4  22119  asclfn  22200  evlslem1  22403  evlsvvval  22414  psdmplcl  22495  psdadd  22496  psdmul  22499  psdmvr  22502  mdetrlin  22929  matunitlindflem1  23006  fncld  23352  hauseqlcld  23977  kqf  24078  filunirn  24213  fmf  24276  txflf  24337  clsnsg  24441  tgpconncomp  24444  qustgpopn  24451  qustgplem  24452  ustfn  24533  xmetunirn  24668  met1stc  24852  rrxmvallem  25737  ovolf  25815  vitali  25946  i1fmulc  26036  mbfi1fseqlem4  26051  itg2seq  26075  itg2monolem1  26083  i1fibl  26140  fncpn  26265  lhop1lem  26345  mdegxrf  26398  aannenlem3  26669  efabl  26890  logccv  27003  gausslemma2dlem1  27705  padicabvf  27970  mpteleeOLD  29485  wlkiswwlks2lem1  30470  clwlkclwwlklem2a2  30596  grpoinvf  31146  occllem  31917  pjfni  32315  pjmfn  32329  rnbra  32721  bra11  32722  kbass2  32731  hmopidmchi  32765  xppreima2  33299  abfmpunirn  33300  psgnfzto1stlem  33714  elrspunidl  34031  locfinreflem  34525  zarclsint  34557  zar0ring  34563  rhmpreimacn  34570  ofcfn  34785  sxbrsigalem3  34957  eulerpartgbij  35057  sseqfv1  35074  sseqfn  35075  sseqf  35077  sseqfv2  35079  signstlen  35249  kardfn  35890  maxssj0  35960  vonf1oonfo  36003  msubrn  36415  msrf  36428  mirimanoffr  36581  faclimlem1  36635  weiunlem  37378  bj-evalfn  38133  bj-inftyexpitaufo  38263  poimirlem30  38708  mblfinlem2  38716  volsupnfl  38723  cnambfre  38726  itg2addnclem2  38730  itg2addnclem3  38731  ftc1anclem5  38755  ftc1anclem7  38757  sdclem2  38816  prdsbnd2  38869  rrncmslem  38906  diafn  42231  cdlemm10N  42315  dibfna  42351  lcfrlem9  42747  mapd1o  42845  hdmapfnN  43026  hgmapfnN  43085  fsuppind  43758  rmxypairf1o  44058  hbtlem6  44271  dgraaf  44289  cytpfn  44343  tfsconcatrev  44490  ntrf  45263  uzmptshftfval  45470  binomcxplemrat  45474  addrfn  45593  subrfn  45594  mulvfn  45595  limsup10exlem  46921  liminfvalxr  46932  fourierdlem62  47317  fourierdlem70  47325  fourierdlem71  47326  cjnpoly  48078  fmtnorn  48758  tposideq  50140  cicfn  50295  fucofn22  50601  fucoid  50609  dfinito4  50775  crosspaltd  51180  crossp3d  51181  veronesevrowd  51193  veronesematrowd  51195  veroquadmodzerod  51198