Theorem fnmpti 6635

Description: Functionality and domain of an ordered-pair class abstraction. (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 3055	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 ∈ V
3		fnmpti.2	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
4	3	mptfng 6631	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴)
5	2, 4	mpbi 230	1 ⊢ 𝐹 Fn 𝐴

Syntax hints:   = wceq 1541   ∈ wcel 2113  ∀wral 3051  Vcvv 3440   ↦ cmpt 5179   Fn wfn 6487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-fun 6494  df-fn 6495

This theorem is referenced by:  dmmpti  6636  fconst  6720  dffn5  6892  idref  7091  eufnfv  7175  offn  7635  caofinvl  7654  fo1st  7953  fo2nd  7954  reldm  7988  fimaproj  8077  mapsnf1o2  8834  unfilem2  9208  fidomdm  9236  noinfep  9571  ssttrcl  9626  ttrcltr  9627  ttrclselem2  9637  aceq3lem  10032  dfac4  10034  ackbij2lem2  10151  cfslb2n  10180  axcc2lem  10348  dmct  10436  konigthlem  10481  rankcf  10690  tskuni  10696  seqf1o  13968  ccatlen  14500  ccatvalfn  14506  swrdlen  14573  swrdwrdsymb  14588  swrdswrd  14630  sqrtf  15289  mptfzshft  15703  efcvgfsum  16011  prmreclem2  16847  1arith  16857  vdwlem6  16916  vdwlem8  16918  slotfn  17113  topnfn  17347  fnmre  17512  cidffn  17603  cidfn  17604  funcres  17822  initofn  17913  termofn  17914  zeroofn  17915  yonedainv  18206  fn0g  18590  smndex1igid  18831  smndex1n0mnd  18839  grpinvfn  18913  cycsubmel  19131  conjnmz  19183  ghmquskerco  19215  psgnfn  19432  odf  19468  sylow1lem4  19532  pgpssslw  19545  sylow2blem3  19553  sylow3lem2  19559  cygctb  19823  dprd2da  19975  fnmgp  20079  zrinitorngc  20577  zrtermorngc  20578  zrtermoringc  20610  rrgsupp  20636  rlmfn  21144  frlmup4  21758  asclfn  21838  evlslem1  22039  evlsvvval  22050  psdmplcl  22107  psdadd  22108  psdmul  22111  psdmvr  22114  mdetrlin  22548  fncld  22968  hauseqlcld  23592  kqf  23693  filunirn  23828  fmf  23891  txflf  23952  clsnsg  24056  tgpconncomp  24059  qustgpopn  24066  qustgplem  24067  ustfn  24148  xmetunirn  24283  met1stc  24467  rrxmvallem  25362  ovolf  25441  vitali  25572  i1fmulc  25662  mbfi1fseqlem4  25677  itg2seq  25701  itg2monolem1  25709  i1fibl  25767  fncpn  25893  lhop1lem  25976  mdegxrf  26031  aannenlem3  26296  efabl  26517  logccv  26630  gausslemma2dlem1  27335  padicabvf  27600  mpteleeOLD  28970  wlkiswwlks2lem1  29944  clwlkclwwlklem2a2  30070  grpoinvf  30609  occllem  31380  pjfni  31778  pjmfn  31792  rnbra  32184  bra11  32185  kbass2  32194  hmopidmchi  32228  xppreima2  32731  abfmpunirn  32732  psgnfzto1stlem  33184  elrspunidl  33511  locfinreflem  33999  zarclsint  34031  zar0ring  34037  rhmpreimacn  34044  ofcfn  34259  sxbrsigalem3  34431  eulerpartgbij  34531  sseqfv1  34548  sseqfn  34549  sseqf  34551  sseqfv2  34553  signstlen  34726  msubrn  35725  msrf  35738  faclimlem1  35939  weiunlem  36659  bj-evalfn  37281  bj-inftyexpitaufo  37409  matunitlindflem1  37819  poimirlem30  37853  mblfinlem2  37861  volsupnfl  37868  cnambfre  37871  itg2addnclem2  37875  itg2addnclem3  37876  ftc1anclem5  37900  ftc1anclem7  37902  sdclem2  37945  prdsbnd2  37998  rrncmslem  38035  diafn  41316  cdlemm10N  41400  dibfna  41436  lcfrlem9  41832  mapd1o  41930  hdmapfnN  42111  hgmapfnN  42170  fsuppind  42854  rmxypairf1o  43174  hbtlem6  43392  dgraaf  43410  cytpfn  43464  tfsconcatrev  43611  ntrf  44385  uzmptshftfval  44608  binomcxplemrat  44612  addrfn  44733  subrfn  44734  mulvfn  44735  limsup10exlem  46037  liminfvalxr  46048  fourierdlem62  46433  fourierdlem70  46441  fourierdlem71  46442  nthrucw  47151  cjnpoly  47156  fmtnorn  47801  tposideq  49154  cicfn  49308  fucofn22  49606  fucoid  49614  dfinito4  49767